Theory Expressiveness_Price
subsection ‹Components of Expressiveness Prices›
theory Expressiveness_Price
imports HML_SRBB Energy
begin
text ‹The (maximal) modal depth (of observations $\langle\alpha\rangle$, $(\alpha)$) is increased on each \<^term>‹Obs› and \<^term>‹BranchConj›.›
primrec
modal_depth_srbb :: ‹('act, 'i) hml_srbb ⇒ enat›
and modal_depth_srbb_inner :: ‹('act, 'i) hml_srbb_inner ⇒ enat›
and modal_depth_srbb_conjunct :: ‹('act, 'i) hml_srbb_conjunct ⇒ enat› where
‹modal_depth_srbb TT = 0› |
‹modal_depth_srbb (Internal χ) = modal_depth_srbb_inner χ› |
‹modal_depth_srbb (ImmConj I ψs) = Sup ((modal_depth_srbb_conjunct ∘ ψs) ` I)› |
‹modal_depth_srbb_inner (Obs α φ) = 1 + modal_depth_srbb φ› |
‹modal_depth_srbb_inner (Conj I ψs) =
Sup ((modal_depth_srbb_conjunct ∘ ψs) ` I)› |
‹modal_depth_srbb_inner (StableConj I ψs) =
Sup ((modal_depth_srbb_conjunct ∘ ψs) ` I)› |
‹modal_depth_srbb_inner (BranchConj a φ I ψs) =
Sup ({1 + modal_depth_srbb φ} ∪ ((modal_depth_srbb_conjunct ∘ ψs) ` I))› |
‹modal_depth_srbb_conjunct (Pos χ) = modal_depth_srbb_inner χ› |
‹modal_depth_srbb_conjunct (Neg χ) = modal_depth_srbb_inner χ›
text ‹The depth of branching conjunctions (with one observation clause not starting with $\langle\varepsilon\rangle$) is increased on each: \<^term>‹BranchConj›.›
primrec
branching_conjunction_depth :: ‹('a, 's) hml_srbb ⇒ enat›
and branch_conj_depth_inner :: ‹('a, 's) hml_srbb_inner ⇒ enat›
and branch_conj_depth_conjunct :: ‹('a, 's) hml_srbb_conjunct ⇒ enat› where
‹branching_conjunction_depth TT = 0› |
‹branching_conjunction_depth (Internal χ) = branch_conj_depth_inner χ› |
‹branching_conjunction_depth (ImmConj I ψs) =
Sup ((branch_conj_depth_conjunct ∘ ψs) ` I)› |
‹branch_conj_depth_inner (Obs _ φ) = branching_conjunction_depth φ› |
‹branch_conj_depth_inner (Conj I ψs) = Sup ((branch_conj_depth_conjunct ∘ ψs) ` I)› |
‹branch_conj_depth_inner (StableConj I ψs) =
Sup ((branch_conj_depth_conjunct ∘ ψs) ` I)› |
‹branch_conj_depth_inner (BranchConj _ φ I ψs) =
1 + Sup ({branching_conjunction_depth φ} ∪ ((branch_conj_depth_conjunct ∘ ψs) ` I))› |
‹branch_conj_depth_conjunct (Pos χ) = branch_conj_depth_inner χ› |
‹branch_conj_depth_conjunct (Neg χ) = branch_conj_depth_inner χ›
text ‹The depth of stable conjunctions (that do enforce stability by a $\neg\langle\tau\rangle\top$-conjunct) is increased on each \<^term>‹StableConj›. Note that if the ‹StableConj› is empty (has no other conjuncts), it is still counted.›
primrec
stable_conjunction_depth :: ‹('a, 's) hml_srbb ⇒ enat›
and st_conj_depth_inner :: ‹('a, 's) hml_srbb_inner ⇒ enat›
and st_conj_depth_conjunct :: ‹('a, 's) hml_srbb_conjunct ⇒ enat› where
‹stable_conjunction_depth TT = 0› |
‹stable_conjunction_depth (Internal χ) = st_conj_depth_inner χ› |
‹stable_conjunction_depth (ImmConj I ψs) = Sup ((st_conj_depth_conjunct ∘ ψs) ` I)› |
‹st_conj_depth_inner (Obs _ φ) = stable_conjunction_depth φ› |
‹st_conj_depth_inner (Conj I ψs) = Sup ((st_conj_depth_conjunct ∘ ψs) ` I)› |
‹st_conj_depth_inner (StableConj I ψs) = 1 + Sup ((st_conj_depth_conjunct ∘ ψs) ` I)› |
‹st_conj_depth_inner (BranchConj _ φ I ψs) =
Sup ({stable_conjunction_depth φ} ∪ ((st_conj_depth_conjunct ∘ ψs) ` I))› |
‹st_conj_depth_conjunct (Pos χ) = st_conj_depth_inner χ› |
‹st_conj_depth_conjunct (Neg χ) = st_conj_depth_inner χ›
text ‹
The depth of unstable conjunctions (that do not enforce stability by a $\neg\langle\tau\rangle\top$-conjunct) is increased on each:
▪ \<^term>‹ImmConj› if there are conjuncts (i.e. $\bigwedge\{\}$ is not counted)
▪ \<^term>‹Conj› if there are conjuncts, (i.e. the conjunction is not empty)
▪ \<^term>‹BranchConj›.
›
primrec
unstable_conjunction_depth :: ‹('a, 's) hml_srbb ⇒ enat›
and inst_conj_depth_inner :: ‹('a, 's) hml_srbb_inner ⇒ enat›
and inst_conj_depth_conjunct :: ‹('a, 's) hml_srbb_conjunct ⇒ enat› where
‹unstable_conjunction_depth TT = 0› |
‹unstable_conjunction_depth (Internal χ) = inst_conj_depth_inner χ› |
‹unstable_conjunction_depth (ImmConj I ψs) =
(if I = {}
then 0
else 1 + Sup ((inst_conj_depth_conjunct ∘ ψs) ` I))› |
‹inst_conj_depth_inner (Obs _ φ) = unstable_conjunction_depth φ› |
‹inst_conj_depth_inner (Conj I ψs) =
(if I = {}
then 0
else 1 + Sup ((inst_conj_depth_conjunct ∘ ψs) ` I))› |
‹inst_conj_depth_inner (StableConj I ψs) =
Sup ((inst_conj_depth_conjunct ∘ ψs) ` I)› |
‹inst_conj_depth_inner (BranchConj _ φ I ψs) =
1 + Sup ({unstable_conjunction_depth φ} ∪ ((inst_conj_depth_conjunct ∘ ψs) ` I))› |
‹inst_conj_depth_conjunct (Pos χ) = inst_conj_depth_inner χ› |
‹inst_conj_depth_conjunct (Neg χ) = inst_conj_depth_inner χ›
text ‹The depth of immediate conjunctions (that are not preceded by $\langle\varepsilon\rangle$)
is increased on each \<^term>‹ImmConj› if there are conjuncts (i.e. $\bigwedge\{\}$ is not counted).›
primrec
immediate_conjunction_depth :: ‹('a, 's) hml_srbb ⇒ enat›
and imm_conj_depth_inner :: ‹('a, 's) hml_srbb_inner ⇒ enat›
and imm_conj_depth_conjunct :: ‹('a, 's) hml_srbb_conjunct ⇒ enat› where
‹immediate_conjunction_depth TT = 0› |
‹immediate_conjunction_depth (Internal χ) = imm_conj_depth_inner χ› |
‹immediate_conjunction_depth (ImmConj I ψs) =
(if I = {}
then 0
else 1 + Sup ((imm_conj_depth_conjunct ∘ ψs) ` I))› |
‹imm_conj_depth_inner (Obs _ φ) = immediate_conjunction_depth φ› |
‹imm_conj_depth_inner (Conj I ψs) = Sup ((imm_conj_depth_conjunct ∘ ψs) ` I)› |
‹imm_conj_depth_inner (StableConj I ψs) = Sup ((imm_conj_depth_conjunct ∘ ψs) ` I)› |
‹imm_conj_depth_inner (BranchConj _ φ I ψs) =
Sup ({immediate_conjunction_depth φ} ∪ ((imm_conj_depth_conjunct ∘ ψs) ` I))› |
‹imm_conj_depth_conjunct (Pos χ) = imm_conj_depth_inner χ› |
‹imm_conj_depth_conjunct (Neg χ) = imm_conj_depth_inner χ›
text ‹The maximal modal depth of positive clauses in conjunctions calculates the modal depth for every positive clause in a conjunction (\<^term>‹Pos χ›).›
primrec
max_positive_conjunct_depth :: ‹('a, 's) hml_srbb ⇒ enat›
and max_pos_conj_depth_inner :: ‹('a, 's) hml_srbb_inner ⇒ enat›
and max_pos_conj_depth_conjunct :: ‹('a, 's) hml_srbb_conjunct ⇒ enat› where
‹max_positive_conjunct_depth TT = 0› |
‹max_positive_conjunct_depth (Internal χ) = max_pos_conj_depth_inner χ› |
‹max_positive_conjunct_depth (ImmConj I ψs) =
Sup ((max_pos_conj_depth_conjunct ∘ ψs) ` I)› |
‹max_pos_conj_depth_inner (Obs _ φ) = max_positive_conjunct_depth φ› |
‹max_pos_conj_depth_inner (Conj I ψs) =
Sup ((max_pos_conj_depth_conjunct ∘ ψs) ` I)› |
‹max_pos_conj_depth_inner (StableConj I ψs) =
Sup ((max_pos_conj_depth_conjunct ∘ ψs) ` I)› |
‹max_pos_conj_depth_inner (BranchConj _ φ I ψs) =
Sup ({1 + modal_depth_srbb φ, max_positive_conjunct_depth φ}
∪ ((max_pos_conj_depth_conjunct ∘ ψs) ` I))› |
‹max_pos_conj_depth_conjunct (Pos χ) = modal_depth_srbb_inner χ› |
‹max_pos_conj_depth_conjunct (Neg χ) = max_pos_conj_depth_inner χ›
text ‹The maximal modal depth of negative clauses in conjunctions calculates the modal depth for every negative clause in a conjunction (\<^term>‹Neg χ›).›
primrec
max_negative_conjunct_depth :: ‹('a, 's) hml_srbb ⇒ enat›
and max_neg_conj_depth_inner :: ‹('a, 's) hml_srbb_inner ⇒ enat›
and max_neg_conj_depth_conjunct :: ‹('a, 's) hml_srbb_conjunct ⇒ enat› where
‹max_negative_conjunct_depth TT = 0› |
‹max_negative_conjunct_depth (Internal χ) = max_neg_conj_depth_inner χ› |
‹max_negative_conjunct_depth (ImmConj I ψs) =
Sup ((max_neg_conj_depth_conjunct ∘ ψs) ` I)› |
‹max_neg_conj_depth_inner (Obs _ φ) = max_negative_conjunct_depth φ› |
‹max_neg_conj_depth_inner (Conj I ψs) =
Sup ((max_neg_conj_depth_conjunct ∘ ψs) ` I)› |
‹max_neg_conj_depth_inner (StableConj I ψs) =
Sup ((max_neg_conj_depth_conjunct ∘ ψs) ` I)› |
‹max_neg_conj_depth_inner (BranchConj _ φ I ψs) =
Sup ({max_negative_conjunct_depth φ} ∪ ((max_neg_conj_depth_conjunct ∘ ψs) ` I))› |
‹max_neg_conj_depth_conjunct (Pos χ) = max_neg_conj_depth_inner χ› |
‹max_neg_conj_depth_conjunct (Neg χ) = modal_depth_srbb_inner χ›
text ‹The depth of negations on a path of the syntax tree) is increased on each \<^term>‹Neg χ›.›
primrec
negation_depth :: ‹('a, 's) hml_srbb ⇒ enat›
and neg_depth_inner :: ‹('a, 's) hml_srbb_inner ⇒ enat›
and neg_depth_conjunct :: ‹('a, 's) hml_srbb_conjunct ⇒ enat› where
‹negation_depth TT = 0› |
‹negation_depth (Internal χ) = neg_depth_inner χ› |
‹negation_depth (ImmConj I ψs) = Sup ((neg_depth_conjunct ∘ ψs) ` I)› |
‹neg_depth_inner (Obs _ φ) = negation_depth φ› |
‹neg_depth_inner (Conj I ψs) = Sup ((neg_depth_conjunct ∘ ψs) ` I)› |
‹neg_depth_inner (StableConj I ψs) = Sup ((neg_depth_conjunct ∘ ψs) ` I)› |
‹neg_depth_inner (BranchConj _ φ I ψs) =
Sup ({negation_depth φ} ∪ ((neg_depth_conjunct ∘ ψs) ` I))› |
‹neg_depth_conjunct (Pos χ) = neg_depth_inner χ› |
‹neg_depth_conjunct (Neg χ) = 1 + neg_depth_inner χ›
subsection ‹Properties of Price Components›
lemma ‹modal_depth_srbb TT = 0›
using Sup_enat_def by simp
lemma ‹modal_depth_srbb (Internal (Obs α (Internal (BranchConj β TT {} ψs2)))) = 2›
using Sup_enat_def by simp
fun observe_n_alphas :: ‹'a ⇒ nat ⇒ ('a, nat) hml_srbb› where
‹observe_n_alphas α 0 = TT› |
‹observe_n_alphas α (Suc n) = Internal (Obs α (observe_n_alphas α n))›
lemma obs_n_α_depth_n: ‹modal_depth_srbb (observe_n_alphas α n) = n›
proof (induct n)
case 0
show ?case unfolding observe_n_alphas.simps(1) and modal_depth_srbb.simps(2)
using zero_enat_def and Sup_enat_def by force
next
case (Suc n)
then show ?case
using eSuc_enat plus_1_eSuc(1) by auto
qed
lemma sup_nats_in_enats_infinite: ‹(SUP x∈ℕ. enat x) = ∞›
by (metis Nats_infinite Sup_enat_def enat.inject finite.emptyI finite_imageD inj_on_def)
lemma sucs_of_nats_in_enats_sup_infinite: ‹(SUP x∈ℕ. 1 + enat x) = ∞›
using sup_nats_in_enats_infinite
by (metis Sup.SUP_cong eSuc_Sup eSuc_infinity image_image image_is_empty plus_1_eSuc(1))
lemma ‹modal_depth_srbb (ImmConj ℕ (λn. Pos (Obs α (observe_n_alphas α n)))) = ∞›
unfolding modal_depth_srbb.simps(3)
and o_def
and modal_depth_srbb_conjunct.simps(1)
and modal_depth_srbb_inner.simps(1)
and obs_n_α_depth_n
by (metis sucs_of_nats_in_enats_sup_infinite)
lemma modal_depth_dominates_pos_conjuncts:
fixes
φ::‹('a, 's) hml_srbb› and
χ::‹('a, 's) hml_srbb_inner› and
ψ::‹('a, 's) hml_srbb_conjunct›
shows
‹(max_positive_conjunct_depth φ ≤ modal_depth_srbb φ)
∧ (max_pos_conj_depth_inner χ ≤ modal_depth_srbb_inner χ)
∧ (max_pos_conj_depth_conjunct ψ ≤ modal_depth_srbb_conjunct ψ)›
using hml_srbb_hml_srbb_inner_hml_srbb_conjunct.induct[of
‹λφ::('a, 's) hml_srbb. max_positive_conjunct_depth φ ≤ modal_depth_srbb φ›
‹λχ. max_pos_conj_depth_inner χ ≤ modal_depth_srbb_inner χ›
‹λψ. max_pos_conj_depth_conjunct ψ ≤ modal_depth_srbb_conjunct ψ›]
by (auto simp add: SUP_mono' add_increasing sup.coboundedI1 sup.coboundedI2)
lemma modal_depth_dominates_neg_conjuncts:
fixes
φ::‹('a, 's) hml_srbb› and
χ::‹('a, 's) hml_srbb_inner› and
ψ::‹('a, 's) hml_srbb_conjunct›
shows
‹(max_negative_conjunct_depth φ ≤ modal_depth_srbb φ)
∧ (max_neg_conj_depth_inner χ ≤ modal_depth_srbb_inner χ)
∧ (max_neg_conj_depth_conjunct ψ ≤ modal_depth_srbb_conjunct ψ)›
using hml_srbb_hml_srbb_inner_hml_srbb_conjunct.induct[of
‹λφ::('a, 's) hml_srbb. max_negative_conjunct_depth φ ≤ modal_depth_srbb φ›
‹λχ. max_neg_conj_depth_inner χ ≤ modal_depth_srbb_inner χ›
‹λψ. max_neg_conj_depth_conjunct ψ ≤ modal_depth_srbb_conjunct ψ›]
by (auto simp add: SUP_mono' add_increasing sup.coboundedI1 sup.coboundedI2)
subsection ‹Expressiveness Price Function›
text ‹The ‹expressiveness_price› function combines the eight component functions into one.›
fun expressiveness_price :: ‹('a, 's) hml_srbb ⇒ energy› where
‹expressiveness_price φ =
E (modal_depth_srbb φ)
(branching_conjunction_depth φ)
(unstable_conjunction_depth φ)
(stable_conjunction_depth φ)
(immediate_conjunction_depth φ)
(max_positive_conjunct_depth φ)
(max_negative_conjunct_depth φ)
(negation_depth φ)›
text ‹Here, we can see the decomposed price of an immediate conjunction:›
lemma expressiveness_price_ImmConj_def:
shows ‹expressiveness_price (ImmConj I ψs) = E
(Sup ((modal_depth_srbb_conjunct ∘ ψs) ` I))
(Sup ((branch_conj_depth_conjunct ∘ ψs) ` I))
(if I = {} then 0 else 1 + Sup ((inst_conj_depth_conjunct ∘ ψs) ` I))
(Sup ((st_conj_depth_conjunct ∘ ψs) ` I))
(if I = {} then 0 else 1 + Sup ((imm_conj_depth_conjunct ∘ ψs) ` I))
(Sup ((max_pos_conj_depth_conjunct ∘ ψs) ` I))
(Sup ((max_neg_conj_depth_conjunct ∘ ψs) ` I))
(Sup ((neg_depth_conjunct ∘ ψs) ` I))› by simp
lemma expressiveness_price_ImmConj_non_empty_def:
assumes ‹I ≠ {}›
shows ‹expressiveness_price (ImmConj I ψs) = E
(Sup ((modal_depth_srbb_conjunct ∘ ψs) ` I))
(Sup ((branch_conj_depth_conjunct ∘ ψs) ` I))
(1 + Sup ((inst_conj_depth_conjunct ∘ ψs) ` I))
(Sup ((st_conj_depth_conjunct ∘ ψs) ` I))
(1 + Sup ((imm_conj_depth_conjunct ∘ ψs) ` I))
(Sup ((max_pos_conj_depth_conjunct ∘ ψs) ` I))
(Sup ((max_neg_conj_depth_conjunct ∘ ψs) ` I))
(Sup ((neg_depth_conjunct ∘ ψs) ` I))› using assms by simp
lemma expressiveness_price_ImmConj_empty_def:
assumes ‹I = {}›
shows ‹expressiveness_price (ImmConj I ψs) = E 0 0 0 0 0 0 0 0› using assms
unfolding expressiveness_price_ImmConj_def by (simp add: bot_enat_def)
text ‹Formalizing HML$_\text{SRBB}$ by mutually recursive data types leads to expressiveness price functions of these other types and corresponding definitions and lemmas.›
fun expr_pr_inner :: ‹('a, 's) hml_srbb_inner ⇒ energy› where
‹expr_pr_inner χ =
E (modal_depth_srbb_inner χ)
(branch_conj_depth_inner χ)
(inst_conj_depth_inner χ)
(st_conj_depth_inner χ)
(imm_conj_depth_inner χ)
(max_pos_conj_depth_inner χ)
(max_neg_conj_depth_inner χ)
(neg_depth_inner χ)›
fun expr_pr_conjunct :: ‹('a, 's) hml_srbb_conjunct ⇒ energy› where
‹expr_pr_conjunct ψ =
E (modal_depth_srbb_conjunct ψ)
(branch_conj_depth_conjunct ψ)
(inst_conj_depth_conjunct ψ)
(st_conj_depth_conjunct ψ)
(imm_conj_depth_conjunct ψ)
(max_pos_conj_depth_conjunct ψ)
(max_neg_conj_depth_conjunct ψ)
(neg_depth_conjunct ψ)›
subsection ‹Prices of Certain Formulas›
context lts_tau
begin
text ‹For example, here, we establish that the expressiveness price of ‹Internal χ› is equal to the expressiveness price of ‹χ›.›
lemma expr_internal_eq:
shows ‹expressiveness_price (Internal χ) = expr_pr_inner χ›
by auto
lemma expr_pos:
assumes ‹expr_pr_inner χ ≤ the (min1_6 e)›
shows ‹expr_pr_conjunct (Pos χ) ≤ e›
using assms by auto
lemma expr_neg:
assumes
‹expr_pr_inner χ ≤ e'›
‹(Option.bind ((subtract_fn 0 0 0 0 0 0 0 1) e) min1_7) = Some e'›
shows ‹expr_pr_conjunct (Neg χ) ≤ e›
proof -
have expr_neg: ‹expr_pr_conjunct (Neg χ) =
E (modal_depth_srbb_conjunct (Neg χ))
(branch_conj_depth_conjunct (Neg χ))
(inst_conj_depth_conjunct (Neg χ))
(st_conj_depth_conjunct (Neg χ))
(imm_conj_depth_conjunct (Neg χ))
(max_pos_conj_depth_conjunct (Neg χ))
(max_neg_conj_depth_conjunct (Neg χ))
(neg_depth_conjunct (Neg χ))›
using expr_pr_conjunct.simps by blast
have neg_ups:
‹modal_depth_srbb_conjunct (Neg χ) = modal_depth_srbb_inner χ›
‹(branch_conj_depth_conjunct (Neg χ)) = branch_conj_depth_inner χ›
‹inst_conj_depth_conjunct (Neg χ) = inst_conj_depth_inner χ›
‹st_conj_depth_conjunct (Neg χ) = st_conj_depth_inner χ›
‹imm_conj_depth_conjunct (Neg χ) = imm_conj_depth_inner χ›
‹max_pos_conj_depth_conjunct (Neg χ) = max_pos_conj_depth_inner χ›
‹max_neg_conj_depth_conjunct (Neg χ) = modal_depth_srbb_inner χ›
‹neg_depth_conjunct (Neg χ) = 1 + neg_depth_inner χ›
by simp+
obtain e1 e2 e3 e4 e5 e6 e7 e8 where e_def: ‹e = E e1 e2 e3 e4 e5 e6 e7 e8›
by (metis energy.exhaust_sel)
hence is_some: ‹(subtract_fn 0 0 0 0 0 0 0 1 e = Some (E e1 e2 e3 e4 e5 e6 e7 (e8-1)))›
using assms bind_eq_None_conv by fastforce
hence ‹modal_depth_srbb_inner χ ≤ (min e1 e7)›
using assms expr_pr_inner.simps leq_components min_1_7_subtr_simp e_def
by (metis energy.sel(1) energy.sel(7) option.discI option.inject)
moreover have ‹neg_depth_inner χ ≤ (e8-1)›
using e_def is_some energy_minus leq_components min_1_7_simps assms
by (smt (verit, ccfv_threshold) bind.bind_lunit energy.sel(8) expr_pr_inner.simps option.sel)
moreover hence ‹neg_depth_conjunct (Neg χ) ≤ e8›
using ‹neg_depth_conjunct (Neg χ) = 1 + neg_depth_inner χ›
by (metis is_some add_diff_assoc_enat add_diff_cancel_enat e_def enat.simps(3)
enat_defs(2) enat_diff_mono energy.sel(8) leq_components linorder_not_less
option.distinct(1) order_le_less)
ultimately show ‹expr_pr_conjunct (Neg χ) ≤ e›
using expr_neg e_def is_some assms neg_ups assms leq_components min_1_7_subtr_simp
by (metis energy.sel expr_pr_inner.simps min.bounded_iff option.distinct(1) option.inject)
qed
lemma expr_obs:
assumes
‹expressiveness_price φ ≤ e'›
‹subtract_fn 1 0 0 0 0 0 0 0 e = Some e'›
shows ‹expr_pr_inner (Obs α φ) ≤ e›
using assms
by (simp) (metis add_diff_cancel_enat add_mono_thms_linordered_semiring(1)
enat.simps(3) enat_defs(2) energy.sel idiff_0_right
le_iff_add le_numeral_extra(4) minus_energy_def option.discI
option.inject)
lemma expr_st_conj:
assumes
‹subtract_fn 0 0 0 1 0 0 0 0 e = Some e'›
‹I ≠ {}›
‹∀q ∈ I. expr_pr_conjunct (ψs q) ≤ e'›
shows
‹expr_pr_inner (StableConj I ψs) ≤ e›
proof -
have st_conj_upds:
‹modal_depth_srbb_inner (StableConj I ψs) = Sup ((modal_depth_srbb_conjunct ∘ ψs) ` I)›
‹branch_conj_depth_inner (StableConj I ψs) = Sup ((branch_conj_depth_conjunct ∘ ψs) ` I)›
‹inst_conj_depth_inner (StableConj I ψs) = Sup ((inst_conj_depth_conjunct ∘ ψs) ` I)›
‹st_conj_depth_inner (StableConj I ψs) = 1 + Sup ((st_conj_depth_conjunct ∘ ψs) ` I)›
‹imm_conj_depth_inner (StableConj I ψs) = Sup ((imm_conj_depth_conjunct ∘ ψs) ` I)›
‹max_pos_conj_depth_inner (StableConj I ψs) = Sup ((max_pos_conj_depth_conjunct∘ψs) ` I)›
‹max_neg_conj_depth_inner (StableConj I ψs) = Sup ((max_neg_conj_depth_conjunct∘ψs) ` I)›
‹neg_depth_inner (StableConj I ψs) = Sup ((neg_depth_conjunct ∘ ψs) ` I)›
by force+
obtain e1 e2 e3 e4 e5 e6 e7 e8 where e_def: ‹e = E e1 e2 e3 e4 e5 e6 e7 e8›
using energy.exhaust_sel by blast
hence is_some: ‹subtract_fn 0 0 0 1 0 0 0 0 e = Some (E e1 e2 e3 (e4-1) e5 e6 e7 e8)›
using assms minus_energy_def
by (smt (verit, del_insts) energy_minus idiff_0_right option.distinct(1))
hence
‹∀i ∈ I. modal_depth_srbb_conjunct (ψs i) ≤ e1›
‹∀i ∈ I. branch_conj_depth_conjunct (ψs i) ≤ e2›
‹∀i ∈ I. inst_conj_depth_conjunct (ψs i) ≤ e3›
‹∀i ∈ I. st_conj_depth_conjunct (ψs i) ≤ (e4 - 1)›
‹∀i ∈ I. imm_conj_depth_conjunct (ψs i) ≤ e5›
‹∀i ∈ I. max_pos_conj_depth_conjunct (ψs i) ≤ e6›
‹∀i ∈ I. max_neg_conj_depth_conjunct (ψs i) ≤ e7›
‹∀i ∈ I. neg_depth_conjunct (ψs i) ≤ e8›
using assms unfolding leq_components by auto
hence sups:
‹Sup ((modal_depth_srbb_conjunct ∘ ψs) ` I) ≤ e1›
‹Sup ((branch_conj_depth_conjunct ∘ ψs) ` I) ≤ e2›
‹Sup ((inst_conj_depth_conjunct ∘ ψs) ` I) ≤ e3›
‹Sup ((st_conj_depth_conjunct ∘ ψs) ` I) ≤ (e4 - 1)›
‹Sup ((imm_conj_depth_conjunct ∘ ψs) ` I) ≤ e5›
‹Sup ((max_pos_conj_depth_conjunct ∘ ψs) ` I) ≤ e6›
‹Sup ((max_neg_conj_depth_conjunct ∘ ψs) ` I) ≤ e7›
‹Sup ((neg_depth_conjunct ∘ ψs) ` I) ≤ e8›
by (simp add: Sup_le_iff)+
hence ‹st_conj_depth_inner (StableConj I ψs) ≤ e4›
using e_def is_some minus_energy_def leq_components st_conj_upds(4)
by (metis add_diff_cancel_enat add_left_mono enat.simps(3) enat_defs(2) energy.sel(4)
le_iff_add option.distinct(1))
then show ?thesis
using st_conj_upds sups
by (simp add: e_def)
qed
lemma expr_imm_conj:
assumes
‹subtract_fn 0 0 0 0 1 0 0 0 e = Some e'›
‹I ≠ {}›
‹expr_pr_inner (Conj I ψs) ≤ e'›
shows ‹expressiveness_price (ImmConj I ψs) ≤ e›
proof -
have conj_upds:
‹modal_depth_srbb_inner (Conj I ψs) = Sup ((modal_depth_srbb_conjunct ∘ ψs) ` I)›
‹branch_conj_depth_inner (Conj I ψs) = Sup ((branch_conj_depth_conjunct ∘ ψs) ` I)›
‹inst_conj_depth_inner (Conj I ψs) = 1 + Sup ((inst_conj_depth_conjunct ∘ ψs) ` I)›
‹st_conj_depth_inner (Conj I ψs) = Sup ((st_conj_depth_conjunct ∘ ψs) ` I)›
‹imm_conj_depth_inner (Conj I ψs) = Sup ((imm_conj_depth_conjunct ∘ ψs) ` I)›
‹max_pos_conj_depth_inner (Conj I ψs) = Sup ((max_pos_conj_depth_conjunct ∘ ψs) ` I)›
‹max_neg_conj_depth_inner (Conj I ψs) = Sup ((max_neg_conj_depth_conjunct ∘ ψs) ` I)›
‹neg_depth_inner (Conj I ψs) = Sup ((neg_depth_conjunct ∘ ψs) ` I)›
using assms
by force+
have imm_conj_upds:
‹modal_depth_srbb (ImmConj I ψs) = Sup ((modal_depth_srbb_conjunct ∘ ψs) ` I)›
‹branching_conjunction_depth (ImmConj I ψs) = Sup ((branch_conj_depth_conjunct∘ψs) ` I)›
‹unstable_conjunction_depth (ImmConj I ψs) = 1 + Sup ((inst_conj_depth_conjunct∘ψs) ` I)›
‹stable_conjunction_depth (ImmConj I ψs) = Sup ((st_conj_depth_conjunct∘ψs) ` I)›
‹immediate_conjunction_depth (ImmConj I ψs) = 1 + Sup ((imm_conj_depth_conjunct∘ψs) ` I)›
‹max_positive_conjunct_depth (ImmConj I ψs) = Sup ((max_pos_conj_depth_conjunct∘ψs) ` I)›
‹max_negative_conjunct_depth (ImmConj I ψs) = Sup ((max_neg_conj_depth_conjunct∘ψs) ` I)›
‹negation_depth (ImmConj I ψs) = Sup ((neg_depth_conjunct∘ψs) ` I)›
using assms
by force+
obtain e1 e2 e3 e4 e5 e6 e7 e8 where e_def: ‹e = E e1 e2 e3 e4 e5 e6 e7 e8›
using assms by (metis energy.exhaust_sel)
hence is_some: ‹(e - (E 0 0 0 0 1 0 0 0)) = (E e1 e2 e3 e4 (e5-1) e6 e7 e8)›
using minus_energy_def
by simp
hence ‹e5>0› using assms(1) e_def leq_components by auto
have
‹E (modal_depth_srbb_inner (Conj I ψs))
(branch_conj_depth_inner (Conj I ψs))
(inst_conj_depth_inner (Conj I ψs))
(st_conj_depth_inner (Conj I ψs))
(imm_conj_depth_inner (Conj I ψs))
(max_pos_conj_depth_inner (Conj I ψs))
(max_neg_conj_depth_inner (Conj I ψs))
(neg_depth_inner (Conj I ψs)) ≤ (E e1 e2 e3 e4 (e5-1) e6 e7 e8)›
using is_some assms
by (metis expr_pr_inner.simps option.discI option.inject)
hence
‹(modal_depth_srbb_inner (Conj I ψs))≤ e1›
‹(branch_conj_depth_inner (Conj I ψs)) ≤ e2›
‹(inst_conj_depth_inner (Conj I ψs)) ≤ e3›
‹(st_conj_depth_inner (Conj I ψs))≤ e4›
‹(imm_conj_depth_inner (Conj I ψs))≤ (e5-1)›
‹(max_pos_conj_depth_inner (Conj I ψs)) ≤ e6›
‹(max_neg_conj_depth_inner (Conj I ψs)) ≤ e7›
‹(neg_depth_inner (Conj I ψs))≤ e8›
by auto
hence E:
‹Sup ((modal_depth_srbb_conjunct ∘ ψs) ` I) ≤ e1›
‹Sup ((branch_conj_depth_conjunct ∘ ψs) ` I) ≤ e2›
‹1 + Sup ((inst_conj_depth_conjunct ∘ ψs) ` I) ≤ e3›
‹Sup ((st_conj_depth_conjunct ∘ ψs) ` I) ≤ e4›
‹Sup ((imm_conj_depth_conjunct ∘ ψs) ` I) ≤ (e5-1)›
‹Sup ((max_pos_conj_depth_conjunct ∘ ψs) ` I) ≤ e6›
‹Sup ((max_neg_conj_depth_conjunct ∘ ψs) ` I) ≤ e7›
‹Sup ((neg_depth_conjunct ∘ ψs) ` I) ≤ e8›
using conj_upds by force+
from this(5) have ‹(1 + Sup ((imm_conj_depth_conjunct ∘ ψs) ` I)) ≤ e5›
using assms(1) ‹e5>0› is_some e_def add.right_neutral
add_diff_cancel_enat enat_add_left_cancel_le ileI1 le_iff_add plus_1_eSuc(1)
by metis
thus ‹expressiveness_price (ImmConj I ψs) ≤ e› using imm_conj_upds E
by (metis e_def energy.sel expressiveness_price.elims leD somewhere_larger_eq)
qed
lemma expr_conj:
assumes
‹subtract_fn 0 0 1 0 0 0 0 0 e = Some e'›
‹I ≠ {}›
‹∀q ∈ I. expr_pr_conjunct (ψs q) ≤ e'›
shows ‹expr_pr_inner (Conj I ψs) ≤ e›
proof -
have conj_upds:
‹modal_depth_srbb_inner (Conj I ψs) = Sup ((modal_depth_srbb_conjunct ∘ ψs) ` I)›
‹branch_conj_depth_inner (Conj I ψs) = Sup ((branch_conj_depth_conjunct ∘ ψs) ` I)›
‹inst_conj_depth_inner (Conj I ψs) = 1 + Sup ((inst_conj_depth_conjunct ∘ ψs) ` I)›
‹st_conj_depth_inner (Conj I ψs) = Sup ((st_conj_depth_conjunct ∘ ψs) ` I)›
‹imm_conj_depth_inner (Conj I ψs) = Sup ((imm_conj_depth_conjunct ∘ ψs) ` I)›
‹max_pos_conj_depth_inner (Conj I ψs) = Sup ((max_pos_conj_depth_conjunct ∘ ψs) ` I)›
‹max_neg_conj_depth_inner (Conj I ψs) = Sup ((max_neg_conj_depth_conjunct ∘ ψs) ` I)›
‹neg_depth_inner (Conj I ψs) = Sup ((neg_depth_conjunct ∘ ψs) ` I)›
using assms by force+
obtain e1 e2 e3 e4 e5 e6 e7 e8 where e_def: ‹e = E e1 e2 e3 e4 e5 e6 e7 e8›
using energy.exhaust_sel by metis
hence is_some: ‹e - (E 0 0 1 0 0 0 0 0) = E e1 e2 (e3-1) e4 e5 e6 e7 e8›
using minus_energy_def by simp
hence ‹e3>0› using assms(1) e_def leq_components by auto
hence
‹∀i ∈ I. modal_depth_srbb_conjunct (ψs i) ≤ e1›
‹∀i ∈ I. branch_conj_depth_conjunct (ψs i) ≤ e2›
‹∀i ∈ I. inst_conj_depth_conjunct (ψs i) ≤ (e3-1)›
‹∀i ∈ I. st_conj_depth_conjunct (ψs i) ≤ e4›
‹∀i ∈ I. imm_conj_depth_conjunct (ψs i) ≤ e5›
‹∀i ∈ I. max_pos_conj_depth_conjunct (ψs i) ≤ e6›
‹∀i ∈ I. max_neg_conj_depth_conjunct (ψs i) ≤ e7›
‹∀i ∈ I. neg_depth_conjunct (ψs i) ≤ e8›
using assms is_some energy.sel leq_components
by (metis expr_pr_conjunct.elims option.distinct(1) option.inject)+
hence sups:
‹Sup ((modal_depth_srbb_conjunct ∘ ψs) ` I) ≤ e1›
‹Sup ((branch_conj_depth_conjunct ∘ ψs) ` I) ≤ e2›
‹Sup ((inst_conj_depth_conjunct ∘ ψs) ` I) ≤ (e3-1)›
‹Sup ((st_conj_depth_conjunct ∘ ψs) ` I) ≤ e4›
‹Sup ((imm_conj_depth_conjunct ∘ ψs) ` I) ≤ e5›
‹Sup ((max_pos_conj_depth_conjunct ∘ ψs) ` I) ≤ e6›
‹Sup ((max_neg_conj_depth_conjunct ∘ ψs) ` I) ≤ e7›
‹Sup ((neg_depth_conjunct ∘ ψs) ` I) ≤ e8›
by (simp add: Sup_le_iff)+
hence ‹inst_conj_depth_inner (Conj I ψs) ≤ e3›
using ‹e3>0› is_some e_def
unfolding conj_upds(3)
by (metis add.right_neutral add_diff_cancel_enat enat_add_left_cancel_le ileI1
le_iff_add plus_1_eSuc(1))
then show ?thesis
using conj_upds sups
by (simp add: e_def)
qed
lemma expr_br_conj:
assumes
‹subtract_fn 0 1 1 0 0 0 0 0 e = Some e'›
‹min1_6 e' = Some e''›
‹subtract_fn 1 0 0 0 0 0 0 0 e'' = Some e'''›
‹expressiveness_price φ ≤ e'''›
‹∀q ∈ Q. expr_pr_conjunct (Φ q) ≤ e'›
‹1 + modal_depth_srbb φ ≤ pos_conjuncts e›
shows ‹expr_pr_inner (BranchConj α φ Q Φ) ≤ e›
proof -
obtain e1 e2 e3 e4 e5 e6 e7 e8 where e_def: ‹e = E e1 e2 e3 e4 e5 e6 e7 e8›
by (smt (z3) energy.exhaust)
hence e'''_def: ‹e''' = (E ((min e1 e6)-1) (e2-1) (e3-1) e4 e5 e6 e7 e8)›
using minus_energy_def
by (smt (z3) assms energy.sel idiff_0_right min_1_6_simps option.distinct(1) option.sel)
hence min_vals: ‹the (min1_6 (e - E 0 1 1 0 0 0 0 0)) - (E 1 0 0 0 0 0 0 0)
= (E ((min e1 e6)-1) (e2-1) (e3-1) e4 e5 e6 e7 e8)›
using assms
by (metis not_Some_eq option.sel)
hence ‹0 < e1› ‹0 < e2› ‹0 < e3› ‹0 < e6›
using assms energy.sel min_1_6_simps
unfolding e_def minus_energy_def leq_components
by (metis (no_types, lifting) gr_zeroI idiff_0_right min_enat_simps(3)
not_one_le_zero option.distinct(1) option.sel, auto)
have e_comp: ‹e - (E 0 1 1 0 0 0 0 0) = E e1 (e2-1) (e3-1) e4 e5 e6 e7 e8› using e_def
by simp
have conj:
‹E (modal_depth_srbb φ)
(branching_conjunction_depth φ)
(unstable_conjunction_depth φ)
(stable_conjunction_depth φ)
(immediate_conjunction_depth φ)
(max_positive_conjunct_depth φ)
(max_negative_conjunct_depth φ)
(negation_depth φ)
≤ ((E ((min e1 e6)-1) (e2-1) (e3-1) e4 e5 e6 e7 e8))›
using assms e'''_def by force
hence conj_single:
‹modal_depth_srbb φ ≤ ((min e1 e6)-1)›
‹branching_conjunction_depth φ ≤ e2 -1›
‹(unstable_conjunction_depth φ) ≤ e3-1›
‹(stable_conjunction_depth φ) ≤ e4›
‹(immediate_conjunction_depth φ) ≤ e5›
‹(max_positive_conjunct_depth φ) ≤ e6›
‹(max_negative_conjunct_depth φ) ≤ e7›
‹(negation_depth φ) ≤ e8›
using leq_components by auto
have ‹0 < (min e1 e6)› using ‹0 < e1› ‹0 < e6›
using min_less_iff_conj by blast
hence ‹1 + modal_depth_srbb φ ≤ (min e1 e6)›
using conj_single add.commute add_diff_assoc_enat add_diff_cancel_enat
add_right_mono conj_single(2) i1_ne_infinity ileI1 one_eSuc
by (metis (no_types, lifting))
hence ‹1 + modal_depth_srbb φ ≤ e1› ‹1 + modal_depth_srbb φ ≤ e6›
using min.bounded_iff by blast+
from conj have ‹1 + branching_conjunction_depth φ ≤ e2›
by (metis ‹0 < e2› add.commute add_diff_assoc_enat add_diff_cancel_enat
add_right_mono conj_single(2) i1_ne_infinity ileI1 one_eSuc)
from conj_single have ‹1 + unstable_conjunction_depth φ ≤ e3›
using ‹0 < e3› add.commute add_diff_assoc_enat add_diff_cancel_enat
add_right_mono conj_single(2) i1_ne_infinity ileI1 one_eSuc
by (metis (no_types, lifting))
have branch: ‹∀q∈Q.
E (modal_depth_srbb_conjunct (Φ q))
(branch_conj_depth_conjunct (Φ q))
(inst_conj_depth_conjunct (Φ q))
(st_conj_depth_conjunct (Φ q))
(imm_conj_depth_conjunct (Φ q))
(max_pos_conj_depth_conjunct (Φ q))
(max_neg_conj_depth_conjunct (Φ q))
(neg_depth_conjunct (Φ q))
≤ (E e1 (e2-1) (e3-1) e4 e5 e6 e7 e8)›
using assms e_def e_comp
by (metis expr_pr_conjunct.simps option.distinct(1) option.sel)
hence branch_single:
‹∀q∈Q. (modal_depth_srbb_conjunct (Φ q)) ≤ e1›
‹∀q∈Q. (branch_conj_depth_conjunct (Φ q)) ≤ (e2-1)›
‹∀q∈Q. (inst_conj_depth_conjunct (Φ q)) ≤ (e3-1)›
‹∀q∈Q. (st_conj_depth_conjunct (Φ q)) ≤ e4›
‹∀q∈Q. (imm_conj_depth_conjunct (Φ q)) ≤ e5›
‹∀q∈Q. (max_pos_conj_depth_conjunct (Φ q)) ≤ e6›
‹∀q∈Q. (max_neg_conj_depth_conjunct (Φ q)) ≤ e7›
‹∀q∈Q. (neg_depth_conjunct (Φ q)) ≤ e8›
by auto
hence ‹∀q∈Q. (1 + branch_conj_depth_conjunct (Φ q)) ≤ e2›
by (metis ‹0 < e2› add.commute add_diff_assoc_enat add_diff_cancel_enat
add_right_mono i1_ne_infinity ileI1 one_eSuc)
from branch_single have ‹∀q∈Q. (1 + inst_conj_depth_conjunct (Φ q)) ≤ e3›
using ‹0 < e3›
by (metis add.commute add_diff_assoc_enat add_diff_cancel_enat add_right_mono
i1_ne_infinity ileI1 one_eSuc)
have
‹expr_pr_inner (BranchConj α φ Q Φ)
= E (modal_depth_srbb_inner (BranchConj α φ Q Φ))
(branch_conj_depth_inner (BranchConj α φ Q Φ))
(inst_conj_depth_inner (BranchConj α φ Q Φ))
(st_conj_depth_inner (BranchConj α φ Q Φ))
(imm_conj_depth_inner (BranchConj α φ Q Φ))
(max_pos_conj_depth_inner (BranchConj α φ Q Φ))
(max_neg_conj_depth_inner (BranchConj α φ Q Φ))
(neg_depth_inner (BranchConj α φ Q Φ))› by simp
hence expr:
‹expr_pr_inner (BranchConj α φ Q Φ)
= E (Sup ({1 + modal_depth_srbb φ} ∪ ((modal_depth_srbb_conjunct ∘ Φ) ` Q)))
(1 + Sup ({branching_conjunction_depth φ} ∪ ((branch_conj_depth_conjunct ∘ Φ) ` Q)))
(1 + Sup ({unstable_conjunction_depth φ} ∪ ((inst_conj_depth_conjunct ∘ Φ) ` Q)))
(Sup ({stable_conjunction_depth φ} ∪ ((st_conj_depth_conjunct ∘ Φ) ` Q)))
(Sup ({immediate_conjunction_depth φ} ∪ ((imm_conj_depth_conjunct ∘ Φ) ` Q)))
(Sup ({1 + modal_depth_srbb φ, max_positive_conjunct_depth φ}
∪ ((max_pos_conj_depth_conjunct ∘ Φ) ` Q)))
(Sup ({max_negative_conjunct_depth φ} ∪ ((max_neg_conj_depth_conjunct ∘ Φ) ` Q)))
(Sup ({negation_depth φ} ∪ ((neg_depth_conjunct ∘ Φ) ` Q)))› by auto
from branch_single ‹1 + modal_depth_srbb φ ≤ e1›
have ‹∀x ∈ ({1 + modal_depth_srbb φ} ∪ ((modal_depth_srbb_conjunct ∘ Φ) ` Q)). x ≤ e1›
by fastforce
hence e1_le:
‹(Sup ({1 + modal_depth_srbb φ} ∪ ((modal_depth_srbb_conjunct ∘ Φ) ` Q))) ≤ e1›
using Sup_least by blast
have ‹∀x ∈ {branching_conjunction_depth φ} ∪ ((branch_conj_depth_conjunct ∘ Φ) ` Q).
x ≤ e2 - 1›
using branch_single conj_single comp_apply image_iff insertE by auto
hence e2_le:
‹1 + Sup ({branching_conjunction_depth φ}
∪ ((branch_conj_depth_conjunct ∘ Φ) ` Q)) ≤ e2›
using Sup_least
by (metis Un_insert_left ‹0 < e2› add.commute eSuc_minus_1 enat_add_left_cancel_le
ileI1 le_iff_add one_eSuc plus_1_eSuc(2) sup_bot_left)
have ‹∀x ∈ ({unstable_conjunction_depth φ} ∪ ((inst_conj_depth_conjunct ∘ Φ) ` Q)).
x ≤ e3-1›
using conj_single branch_single
using comp_apply image_iff insertE by auto
hence e3_le:
‹1 + Sup ({unstable_conjunction_depth φ} ∪ ((inst_conj_depth_conjunct ∘ Φ) ` Q)) ≤ e3›
using Un_insert_left ‹0<e3› add.commute eSuc_minus_1 enat_add_left_cancel_le ileI1
le_iff_add one_eSuc plus_1_eSuc(2) sup_bot_left
by (metis Sup_least)
have fa:
‹∀x ∈ ({stable_conjunction_depth φ} ∪ ((st_conj_depth_conjunct ∘ Φ) ` Q)). x ≤ e4›
‹∀x ∈ ({immediate_conjunction_depth φ} ∪ ((imm_conj_depth_conjunct ∘ Φ) ` Q)). x ≤ e5›
‹∀x ∈ ({1 + modal_depth_srbb φ, max_positive_conjunct_depth φ}
∪ ((max_pos_conj_depth_conjunct ∘ Φ) ` Q)). x ≤ e6›
‹∀x ∈ ({max_negative_conjunct_depth φ}
∪ ((max_neg_conj_depth_conjunct ∘ Φ) ` Q)). x ≤ e7›
‹∀x ∈ ({negation_depth φ} ∪ ((neg_depth_conjunct ∘ Φ) ` Q)). x ≤ e8›
using conj_single branch_single ‹1 + modal_depth_srbb φ ≤ e6› by auto
hence
‹(Sup ({stable_conjunction_depth φ} ∪ ((st_conj_depth_conjunct ∘ Φ) ` Q))) ≤ e4›
‹(Sup ({immediate_conjunction_depth φ} ∪ ((imm_conj_depth_conjunct ∘ Φ) ` Q))) ≤ e5›
‹(Sup ({1 + modal_depth_srbb φ, max_positive_conjunct_depth φ}
∪ ((max_pos_conj_depth_conjunct ∘ Φ) ` Q))) ≤ e6›
‹(Sup ({max_negative_conjunct_depth φ} ∪ ((max_neg_conj_depth_conjunct ∘ Φ) ` Q))) ≤ e7›
‹(Sup ({negation_depth φ} ∪ ((neg_depth_conjunct ∘ Φ) ` Q))) ≤ e8›
using Sup_least
by metis+
thus ‹expr_pr_inner (BranchConj α φ Q Φ) ≤ e›
using expr e3_le e2_le e1_le e_def energy.sel leq_components by presburger
qed
lemma expressiveness_price_ImmConj_geq_parts:
assumes ‹i ∈ I›
shows ‹expressiveness_price (ImmConj I ψs) - E 0 0 1 0 1 0 0 0 ≥ expr_pr_conjunct (ψs i)›
proof -
from assms have ‹I ≠ {}› by blast
from expressiveness_price_ImmConj_non_empty_def[OF ‹I ≠ {}›]
have ‹expressiveness_price (ImmConj I ψs) ≥ E 0 0 1 0 1 0 0 0›
using energy_leq_cases by force
hence
‹expressiveness_price (ImmConj I ψs) - E 0 0 1 0 1 0 0 0 = E
(Sup ((modal_depth_srbb_conjunct ∘ ψs) ` I))
(Sup ((branch_conj_depth_conjunct ∘ ψs) ` I))
(Sup ((inst_conj_depth_conjunct ∘ ψs) ` I))
(Sup ((st_conj_depth_conjunct ∘ ψs) ` I))
(Sup ((imm_conj_depth_conjunct ∘ ψs) ` I))
(Sup ((max_pos_conj_depth_conjunct ∘ ψs) ` I))
(Sup ((max_neg_conj_depth_conjunct ∘ ψs) ` I))
(Sup ((neg_depth_conjunct ∘ ψs) ` I))›
unfolding expressiveness_price_ImmConj_non_empty_def[OF ‹I ≠ {}›]
by simp
also have ‹... ≥ expr_pr_conjunct (ψs i)›
using assms ‹I ≠ {}› SUP_upper unfolding leq_components by fastforce
finally show ?thesis .
qed
lemma expressiveness_price_ImmConj_geq_parts':
assumes ‹i ∈ I›
shows
‹(expressiveness_price (ImmConj I ψs) - E 0 0 0 0 1 0 0 0) - E 0 0 1 0 0 0 0 0
≥ expr_pr_conjunct (ψs i)›
using expressiveness_price_ImmConj_geq_parts[OF assms]
less_eq_energy_def minus_energy_def
by (smt (z3) energy.sel idiff_0_right)
text ‹Here, we show the prices for some specific formulas.›
lemma example_φ_cp:
fixes op a b::‹'a› and left right::‹'s›
defines ‹φ ≡
(Internal
(Obs op
(Internal
(Conj {left, right}
(λi. (if i = left
then (Pos (Obs a TT))
else if i = right
then (Pos (Obs b TT))
else undefined))))))›
shows
‹modal_depth_srbb φ = 2›
‹branching_conjunction_depth φ = 0›
‹unstable_conjunction_depth φ = 1›
‹stable_conjunction_depth φ = 0›
‹immediate_conjunction_depth φ = 0›
‹max_positive_conjunct_depth φ = 1›
‹max_negative_conjunct_depth φ = 0›
‹negation_depth φ = 0›
unfolding φ_def by simp+
lemma ‹expressiveness_price (Internal
(Obs op
(Internal
(Conj {left, right}
(λi. (if i = left
then (Pos (Obs a TT))
else if i = right
then (Pos (Obs b TT))
else undefined)))))) = E 2 0 1 0 0 1 0 0›
by simp
lemma ‹expressiveness_price TT = E 0 0 0 0 0 0 0 0›
by simp
lemma ‹expressiveness_price (ImmConj {} ψs) = E 0 0 0 0 0 0 0 0›
by (simp add: Sup_enat_def)
lemma ‹expressiveness_price (Internal (Conj {} ψs)) = E 0 0 0 0 0 0 0 0›
by (simp add: Sup_enat_def)
lemma ‹expressiveness_price (Internal (BranchConj α TT {} ψs)) = E 1 1 1 0 0 1 0 0›
by (simp add: Sup_enat_def)
lemma expr_obs_phi:
‹subtract_fn 1 0 0 0 0 0 0 0 (expr_pr_inner (Obs α φ)) = Some (expressiveness_price φ)›
by simp
end
subsection ‹Characterizing Equivalence by Energy Coordinates›
text ‹
We can now define a sublanguage of Hennessy--Milner Logic ‹𝒪› by the set of formulas with prices below an energy coordinate.
›
definition 𝒪 :: ‹energy ⇒ (('a, 's) hml_srbb) set› where
‹𝒪 energy ≡ {φ . expressiveness_price φ ≤ energy}›
lemma 𝒪_sup: ‹UNIV = 𝒪 (E ∞ ∞ ∞ ∞ ∞ ∞ ∞ ∞)› unfolding 𝒪_def by auto
lemma price_hierarchy_entails_modal_hierarchy:
assumes ‹e1 ≤ e2›
shows ‹𝒪 e1 ⊆ 𝒪 e2›
using assms unfolding 𝒪_def by auto
definition 𝒪_inner :: ‹energy ⇒ (('a, 's) hml_srbb_inner) set› where
‹𝒪_inner energy ≡ {χ . expr_pr_inner χ ≤ energy}›
definition 𝒪_conjunct :: ‹energy ⇒ (('a, 's) hml_srbb_conjunct) set› where
‹𝒪_conjunct energy ≡ {χ . expr_pr_conjunct χ ≤ energy}›
context lts_tau
begin
text ‹A state ‹p› pre-orders another state ‹q› with respect to some energy ‹e› if and only if ‹p› HML pre-orders ‹q› with respect to the HML sublanguage \<^term>‹𝒪 e›.›
definition expr_preord :: ‹'s ⇒ energy ⇒ 's ⇒ bool› (‹_ ≼ _ _› 60) where
‹(p ≼ e q) ≡ preordered (𝒪 e) p q›
text ‹Conversely, ‹p› and ‹q› are equivalent with respect to ‹e› if and only if they are equivalent with respect to that HML sublanguage \<^term>‹𝒪 e›.›
definition expr_equiv :: ‹'s ⇒ energy ⇒ 's ⇒ bool› (‹_ ∼ _ _› 60) where
‹(p ∼ e q) ≡ equivalent (𝒪 e) p q›
lemma price_hierachy_preorder_dual:
assumes
‹e1 ≤ e2›
‹p ≼ e2 q›
shows
‹p ≼ e1 q›
using assms price_hierarchy_entails_modal_hierarchy expr_preord_def by auto
subsection ‹Relational Effects of Prices›
text ‹
Certain properties of prices influence the preorder/equivalence relations that are characterized by price coordinates. (This will be important for some behavioral equivalences that we will prove to be characterized by specific prices.)
›
lemma distinction_combination_eta:
fixes p q
defines
‹Qα ≡ {q'. q ↠ q' ∧ (∄φ. φ ∈ 𝒪 (E ∞ ∞ ∞ 0 0 ∞ 0 0) ∧ distinguishes φ p q')}›
assumes
‹p ↦a α p'›
‹∀q'∈ Qα.
∀q'' q'''. q' ↦a α q'' ⟶ q'' ↠ q''' ⟶ distinguishes (Φ q''') p' q'''›
shows
‹∀q'∈ Qα. hml_srbb_inner.distinguishes (Obs α (Internal (Conj
{q'''. ∃q'∈ Qα. ∃q''. q' ↦a α q'' ∧ q'' ↠ q'''}
(conjunctify_distinctions Φ p')))) p q'›
proof -
have ‹∀q'∈ Qα. ∀q'''∈{q'''. ∃q'∈ Qα. ∃q''. q' ↦a α q'' ∧ q'' ↠ q'''}.
hml_srbb_conj.distinguishes ((conjunctify_distinctions Φ p') q''') p' q'''›
proof clarify
fix q' q'' q'''
assume ‹q' ∈ Qα› ‹q' ↦a α q''› ‹q'' ↠ q'''›
thus ‹hml_srbb_conj.distinguishes (conjunctify_distinctions Φ p' q''') p' q'''›
using assms(3) distinction_conjunctification by blast
qed
hence ‹∀q'∈ Qα. ∀q''. q' ↦a α q''
⟶ distinguishes (Internal (Conj {q'''. ∃q'∈ Qα. ∃q''. q' ↦a α q'' ∧ q'' ↠ q'''}
(conjunctify_distinctions Φ p'))) p' q''›
using silent_reachable.refl unfolding Qα_def by fastforce
thus ‹∀q'∈ Qα.
hml_srbb_inner.distinguishes (Obs α (Internal (Conj
{q'''. ∃q'∈ Qα. ∃q''. q' ↦a α q'' ∧ q'' ↠ q'''}
(conjunctify_distinctions Φ p')))) p q'›
using assms(2) by (auto) (metis silent_reachable.refl)+
qed
lemma distinction_conjunctification_two_way_price:
assumes
‹∀q∈I. distinguishes (Φ q) p q ∨ distinguishes (Φ q) q p›
‹∀q∈I. Φ q ∈ 𝒪 (E ∞ ∞ ∞ 0 0 ∞ ∞ ∞)›
shows
‹∀q∈I.
(if distinguishes (Φ q) p q
then conjunctify_distinctions
else conjunctify_distinctions_dual
) Φ p q ∈ 𝒪_conjunct (E ∞ ∞ ∞ 0 0 ∞ ∞ ∞)›
proof
fix q
assume ‹q ∈ I›
show
‹(if distinguishes (Φ q) p q
then conjunctify_distinctions
else conjunctify_distinctions_dual
) Φ p q ∈ 𝒪_conjunct (E ∞ ∞ ∞ 0 0 ∞ ∞ ∞)›
proof (cases ‹Φ q›)
case TT
then show ?thesis
using assms ‹q ∈ I›
by fastforce
next
case (Internal χ)
then show ?thesis
using assms ‹q ∈ I›
unfolding conjunctify_distinctions_def conjunctify_distinctions_dual_def 𝒪_def 𝒪_conjunct_def
by fastforce
next
case (ImmConj J Ψ)
hence ‹J = {}›
using assms ‹q ∈ I› unfolding 𝒪_def
by (simp, metis iadd_is_0 immediate_conjunction_depth.simps(3) zero_one_enat_neq(1))
then show ?thesis
using assms ‹q ∈ I› ImmConj by fastforce
qed
qed
lemma distinction_combination_eta_two_way:
fixes p q p' Φ
defines
‹Qα ≡ {q'. q ↠ q' ∧ (∄φ. φ ∈ 𝒪 (E ∞ ∞ ∞ 0 0 ∞ ∞ ∞)
∧ (distinguishes φ p q' ∨ distinguishes φ q' p))}› and
‹Ψα ≡ λq'''. (
if distinguishes (Φ q''') p' q'''
then conjunctify_distinctions
else conjunctify_distinctions_dual
) Φ p' q'''›
assumes
‹p ↦a α p'›
‹∀q'∈ Qα.
∀q'' q'''. q' ↦a α q'' ⟶ q'' ↠ q'''
⟶ distinguishes (Φ q''') p' q''' ∨ distinguishes (Φ q''') q''' p'›
shows
‹∀q'∈ Qα. hml_srbb_inner.distinguishes (Obs α (Internal (Conj
{q'''. ∃q'∈ Qα. ∃q''. q' ↦a α q'' ∧ q'' ↠ q'''}
Ψα))) p q'›
proof -
have ‹∀q'∈ Qα. ∀q'''∈{q'''. ∃q'∈ Qα. ∃q''. q' ↦a α q'' ∧ q'' ↠ q'''}.
hml_srbb_conj.distinguishes (Ψα q''') p' q'''›
proof clarify
fix q' q'' q'''
assume ‹q' ∈ Qα› ‹q' ↦a α q''› ‹q'' ↠ q'''›
thus ‹hml_srbb_conj.distinguishes (Ψα q''') p' q''' ›
using assms(4) Ψα_def distinction_conjunctification_two_way mem_Collect_eq
by (smt (verit, best))
qed
hence ‹∀q'∈ Qα. ∀q'''∈{q'''. ∃q'∈ Qα. ∃q''. q' ↦a α q'' ∧ q'' ↠ q'''}.
hml_srbb_inner.distinguishes (Conj {q'''. ∃q'∈ Qα. ∃q''. q' ↦a α q'' ∧ q'' ↠ q'''}
Ψα) p' q'''›
using srbb_dist_conjunct_implies_dist_conjunction
unfolding lts_semantics.distinguishes_def
by (metis (no_types, lifting))
hence ‹∀q'∈ Qα. ∀q'''. (∃q''. q' ↦a α q'' ∧ q'' ↠ q''') ⟶
hml_srbb_inner.distinguishes
(Conj {q'''. ∃q'∈ Qα. ∃q''. q' ↦a α q'' ∧ q'' ↠ q'''} Ψα) p' q'''›
by blast
hence ‹∀q'∈ Qα. ∀q''. q' ↦a α q'' ⟶ distinguishes
(Internal (Conj {q'''. ∃q'∈ Qα. ∃q''. q' ↦a α q'' ∧ q'' ↠ q'''} Ψα)) p' q''›
by (meson distinguishes_def hml_srbb_inner.distinguishes_def
hml_srbb_models.simps(2) silent_reachable.refl)
thus ‹∀q'∈ Qα. hml_srbb_inner.distinguishes
(Obs α (Internal (Conj {q'''. ∃q'∈ Qα. ∃q''. q' ↦a α q'' ∧ q'' ↠ q'''} Ψα))) p q'›
using assms(3)
by auto (metis silent_reachable.refl)+
qed
lemma distinction_conjunctification_price:
assumes
‹∀q∈I. distinguishes (Φ q) p q›
‹∀q∈I. Φ q ∈ 𝒪 pr›
‹modal_depth pr ≤ pos_conjuncts pr›
shows
‹∀q∈I. ((conjunctify_distinctions Φ p) q) ∈ 𝒪_conjunct pr›
proof
fix q
assume ‹q ∈ I›
show ‹conjunctify_distinctions Φ p q ∈ 𝒪_conjunct pr›
proof (cases ‹Φ q›)
case TT
then show ?thesis
using assms ‹q ∈ I›
by fastforce
next
case (Internal χ)
then show ?thesis
using assms ‹q ∈ I›
unfolding conjunctify_distinctions_def 𝒪_def 𝒪_conjunct_def
by fastforce
next
case (ImmConj J Ψ)
hence ‹∃i. i∈J ∧ hml_srbb_conj.distinguishes (Ψ i) p q›
using ‹q ∈ I› assms(1) by fastforce
moreover have ‹conjunctify_distinctions Φ p q
= Ψ (SOME i. i∈J ∧ hml_srbb_conj.distinguishes (Ψ i) p q)›
unfolding ImmConj conjunctify_distinctions_def by simp
ultimately have Ψ_i:
‹∃i∈J. hml_srbb_conj.distinguishes (Ψ i) p q ∧ conjunctify_distinctions Φ p q = Ψ i›
by (metis (no_types, lifting) some_eq_ex)
hence ‹conjunctify_distinctions Φ p q ∈ Ψ`J›
unfolding image_iff by blast
hence
‹expr_pr_conjunct (conjunctify_distinctions Φ p q)
≤ expressiveness_price (ImmConj J Ψ)›
by (smt (verit, best) Ψ_i dual_order.trans expressiveness_price_ImmConj_geq_parts
gets_smaller)
then show ?thesis
using assms ‹q ∈ I› ImmConj unfolding 𝒪_def 𝒪_conjunct_def by auto
qed
qed
lemma modal_stability_respecting:
‹stability_respecting (preordered (𝒪 (E e1 e2 e3 ∞ e5 ∞ e7 e8)))›
unfolding stability_respecting_def
proof safe
fix p q
assume p_stability:
‹preordered (𝒪 (E e1 e2 e3 ∞ e5 ∞ e7 e8)) p q›
‹stable_state p›
have ‹¬(∀q'. q ↠ q'
⟶ ¬ preordered (𝒪 (E e1 e2 e3 ∞ e5 ∞ e7 e8)) p q' ∨ ¬ stable_state q')›
proof safe
assume ‹∀q'. q ↠ q'
⟶ ¬ preordered (𝒪 (E e1 e2 e3 ∞ e5 ∞ e7 e8)) p q' ∨ ¬ stable_state q'›
hence ‹∀q'. q ↠ q' ⟶ stable_state q'
⟶ (∃φ ∈ 𝒪 (E e1 e2 e3 ∞ e5 ∞ e7 e8). distinguishes φ p q')› by auto
then obtain Φ where Φ_def:
‹∀q'∈(silent_reachable_set {q}). stable_state q'
⟶ distinguishes (Φ q') p q' ∧ Φ q' ∈ 𝒪 (E e1 e2 e3 ∞ e5 ∞ e7 e8)›
using singleton_iff sreachable_set_is_sreachable by metis
hence distinctions:
‹∀q'∈(silent_reachable_set {q} ∩ {q'. stable_state q'}). distinguishes (Φ q') p q'›
‹∀q'∈(silent_reachable_set {q} ∩ {q'. stable_state q'}).
Φ q' ∈ 𝒪 (E e1 e2 e3 ∞ e5 ∞ e7 e8)› by blast+
from distinction_conjunctification_price[OF this] have
‹∀q'∈(silent_reachable_set {q} ∩ {q'. stable_state q'}).
conjunctify_distinctions Φ p q' ∈ 𝒪_conjunct (E e1 e2 e3 ∞ e5 ∞ e7 e8)›
by fastforce
hence conj_price: ‹StableConj (silent_reachable_set {q} ∩ {q'. stable_state q'})
(conjunctify_distinctions Φ p) ∈ 𝒪_inner (E e1 e2 e3 ∞ e5 ∞ e7 e8)›
unfolding 𝒪_inner_def 𝒪_conjunct_def using SUP_le_iff by fastforce
from Φ_def have
‹∀q'∈(silent_reachable_set {q}). stable_state q'
⟶ hml_srbb_conj.distinguishes (conjunctify_distinctions Φ p q') p q'›
using singleton_iff distinction_conjunctification by metis
hence ‹hml_srbb_inner.distinguishes_from
(StableConj (silent_reachable_set {q} ∩ {q'. stable_state q'})
(conjunctify_distinctions Φ p)) p (silent_reachable_set {q})›
using p_stability(2) by fastforce
hence
‹distinguishes
(Internal (StableConj (silent_reachable_set {q} ∩ {q'. stable_state q'})
(conjunctify_distinctions Φ p))
)
p q›
unfolding silent_reachable_set_def
using silent_reachable.refl by auto
moreover have
‹Internal (StableConj (silent_reachable_set {q} ∩ {q'. stable_state q'})
(conjunctify_distinctions Φ p)) ∈ 𝒪 (E e1 e2 e3 ∞ e5 ∞ e7 e8)›
using conj_price unfolding 𝒪_def 𝒪_inner_def by simp
ultimately show False
using p_stability(1) preordered_no_distinction by blast
qed
thus ‹∃q'. q ↠ q' ∧ preordered (𝒪 (E e1 e2 e3 ∞ e5 ∞ e7 e8)) p q' ∧ stable_state q'›
by blast
qed
end
end