Theory MLTL_Properties
section ‹ Properties of MLTL ›
theory MLTL_Properties
imports MLTL_Encoding
begin
subsection ‹Useful Functions›
text ‹ We use the following function to assume that an MLTL formula is well-defined:
i.e., that all intervals in the formula satisfy a is less than or equal to b ›
fun intervals_welldef:: "'a mltl ⇒ bool"
where "intervals_welldef True⇩m = True"
| "intervals_welldef False⇩m = True"
| "intervals_welldef (Prop⇩m (p)) = True"
| "intervals_welldef (Not⇩m φ) = intervals_welldef φ"
| "intervals_welldef (φ And⇩m ψ) = (intervals_welldef φ ∧ intervals_welldef ψ)"
| "intervals_welldef (φ Or⇩m ψ) = (intervals_welldef φ ∧ intervals_welldef ψ)"
| "intervals_welldef (F⇩m [a,b] φ) = (a ≤ b ∧ intervals_welldef φ)"
| "intervals_welldef (G⇩m [a,b] φ) = (a ≤ b ∧ intervals_welldef φ)"
| "intervals_welldef (φ U⇩m [a,b] ψ) =
(a ≤ b ∧ intervals_welldef φ ∧ intervals_welldef ψ)"
| "intervals_welldef (φ R⇩m [a,b] ψ) =
(a ≤ b ∧ intervals_welldef φ ∧ intervals_welldef ψ)"
subsection ‹Semantic Equivalence›
definition semantic_equiv:: "'a mltl ⇒ 'a mltl ⇒ bool" ("_ ≡⇩m _" [80, 80] 80)
where "φ ≡⇩m ψ ≡ (∀π. π ⊨⇩m φ = π ⊨⇩m ψ)"
fun depth_mltl:: "'a mltl ⇒ nat"
where "depth_mltl True⇩m = 0"
| "depth_mltl False⇩m = 0"
| "depth_mltl Prop⇩m (p) = 0"
| "depth_mltl (Not⇩m φ) = 1 + depth_mltl φ"
| "depth_mltl (φ And⇩m ψ) = 1 + max (depth_mltl φ) (depth_mltl ψ)"
| "depth_mltl (φ Or⇩m ψ) = 1 + max (depth_mltl φ) (depth_mltl ψ)"
| "depth_mltl (G⇩m [a,b] φ) = 1 + depth_mltl φ"
| "depth_mltl (F⇩m [a,b] φ) = 1 + depth_mltl φ"
| "depth_mltl (φ U⇩m [a,b] ψ) = 1 + max (depth_mltl φ) (depth_mltl ψ)"
| "depth_mltl (φ R⇩m [a,b] ψ) = 1 + max (depth_mltl φ) (depth_mltl ψ)"
fun subformulas:: "'a mltl ⇒ 'a mltl set"
where "subformulas True⇩m = {}"
| "subformulas False⇩m = {}"
| "subformulas Prop⇩m (p) = {}"
| "subformulas (Not⇩m φ) = {φ} ∪ subformulas φ"
| "subformulas (φ And⇩m ψ) = {φ, ψ} ∪ subformulas φ ∪ subformulas ψ"
| "subformulas (φ Or⇩m ψ) = {φ, ψ} ∪ subformulas φ ∪ subformulas ψ"
| "subformulas (G⇩m [a,b] φ) = {φ} ∪ subformulas φ"
| "subformulas (F⇩m [a,b] φ) = {φ} ∪ subformulas φ"
| "subformulas (φ U⇩m [a,b] ψ) = {φ, ψ} ∪ subformulas φ ∪ subformulas ψ"
| "subformulas (φ R⇩m [a,b] ψ) = {φ, ψ} ∪ subformulas φ ∪ subformulas ψ"
subsection ‹Basic Properties›
lemma future_or_distribute:
shows "F⇩m [a,b] (φ1 Or⇩m φ2) ≡⇩m (F⇩m [a,b] φ1) Or⇩m (F⇩m [a,b] φ2)"
unfolding semantic_equiv_def by auto
lemma global_and_distribute:
shows "G⇩m [a,b] (φ1 And⇩m φ2) ≡⇩m (G⇩m [a,b] φ1) And⇩m (G⇩m [a,b] φ2)"
unfolding semantic_equiv_def
unfolding semantics_mltl.simps by auto
lemma not_not_equiv:
shows "φ ≡⇩m (Not⇩m (Not⇩m φ))"
unfolding semantic_equiv_def by simp
lemma demorgan_and_or:
shows "Not⇩m (φ And⇩m ψ) ≡⇩m (Not⇩m φ) Or⇩m (Not⇩m ψ)"
unfolding semantic_equiv_def by simp
lemma demorgan_or_and:
shows "semantic_equiv (Not_mltl (φ Or⇩m ψ))
(And_mltl (Not⇩m φ) (Not_mltl ψ))"
unfolding semantic_equiv_def by simp
lemma future_as_until:
fixes a b::"nat"
assumes "a ≤ b"
shows "(F⇩m [a,b] φ) ≡⇩m (True⇩m U⇩m [a,b] φ)"
unfolding semantic_equiv_def by auto
lemma globally_as_release:
fixes a b::"nat"
assumes "a ≤ b"
shows "(G⇩m [a,b] φ) ≡⇩m (False⇩m R⇩m [a,b] φ)"
unfolding semantic_equiv_def by auto
lemma until_or_distribute:
fixes a b ::"nat"
assumes "a ≤ b"
shows "φ U⇩m [a,b] (α Or⇩m β) ≡⇩m
(φ U⇩m [a,b] α) Or⇩m (φ U⇩m [a,b] β)"
using assms semantics_mltl.simps unfolding semantic_equiv_def
by auto
lemma until_and_distribute:
fixes a b ::"nat"
assumes "a ≤ b"
shows "(α And⇩m β) U⇩m [a,b] φ ≡⇩m
(α U⇩m [a,b] φ) And⇩m (β U⇩m [a,b] φ)"
using assms unfolding semantic_equiv_def semantics_mltl.simps
by (smt (verit) linorder_less_linear order_less_trans)
lemma release_or_distribute:
fixes a b ::"nat"
assumes "a ≤ b"
shows "(α Or⇩m β) R⇩m [a,b] φ ≡⇩m
(α R⇩m [a,b] φ) Or⇩m (β R⇩m [a,b] φ)"
using assms unfolding semantic_equiv_def semantics_mltl.simps
by auto
lemma different_next_operators:
shows "¬(G⇩m [1,1] φ ≡⇩m F⇩m [1,1] φ)"
unfolding semantic_equiv_def semantics_mltl.simps
by (metis le_numeral_extra(4) linordered_nonzero_semiring_class.zero_le_one list.size(3) not_one_less_zero)
subsection ‹Duality Properties›
lemma globally_future_dual:
fixes a b::"nat"
assumes "a ≤ b"
shows "(G⇩m [a,b] φ) ≡⇩m Not⇩m (F⇩m [a,b] (Not⇩m φ))"
using assms unfolding semantic_equiv_def by auto
lemma future_globally_dual:
fixes a b::"nat"
assumes "a ≤ b"
shows "(F⇩m [a,b] φ) ≡⇩m Not⇩m (G⇩m [a,b] (Not⇩m φ))"
using assms unfolding semantic_equiv_def by auto
text ‹ Proof altered from source material in the last case. ›
lemma release_until_dual1:
fixes a b::"nat"
assumes "π ⊨⇩m (φ R⇩m [a,b] ψ)"
shows "π ⊨⇩m (Not⇩m ((Not⇩m φ) U⇩m [a,b] (Not⇩m ψ)))"
proof -
have relase_unfold: "(a ≤ b ∧ (length π ≤ a ∨ (∀i::nat. (i ≥ a ∧ i ≤ b) ⟶ ((semantics_mltl (drop i π) ψ) ∨ (∃j. j ≥ a ∧ j ≤ b-1 ∧ semantics_mltl (drop j π) φ ∧ (∀k. a ≤ k ∧ k ≤ j ⟶ semantics_mltl (drop k π) ψ))))))"
using assms by auto
{assume *: "length π ≤ a"
then have ?thesis
by (simp add: assms)
} moreover {assume **: "(∀i. (a ≤ i ∧ i ≤ b) ⟶ semantics_mltl (drop i π) ψ)"
then have "length π ≤ a ∨ (∀s. a ≤ s ∧ s ≤ b ⟶ (semantics_mltl (drop s π) ψ ∨ (∃t. t≥ a ∧ t ≤ s-1 ∧ semantics_mltl (drop t π) φ)))"
by auto
then have ?thesis using assms
using "**" linorder_not_less by auto
} moreover {assume *: "length π > a ∧ (∃i. (a ≤ i ∧ i ≤ b) ∧ ¬ (semantics_mltl (drop i π) ψ))"
then obtain i where i_prop: "(a ≤ i ∧ i ≤ b)" "¬ (semantics_mltl (drop i π) ψ)"
by blast
have "(∀i. (a ≤ i ∧ i ≤ b) ⟶ (semantics_mltl (drop i π) ψ))
⟶ semantics_mltl (drop i π) ψ"
using i_prop(1) by blast
then have h1: "¬ (∀i. (a ≤ i ∧ i ≤ b) ⟶
semantics_mltl (drop i π) ψ)"
using i_prop by blast
have "(∀i. a ≤ i ∧ i ≤ b ⟶
semantics_mltl (drop i π) ψ) ∨
(∃j≥a. j ≤ b - 1 ∧
semantics_mltl (drop j π) φ ∧
(∀k. a ≤ k ∧ k ≤ j ⟶
semantics_mltl (drop k π) ψ))"
using * relase_unfold by auto
then have "(∃j≥a. j ≤ b - 1 ∧
semantics_mltl (drop j π) φ ∧
(∀k. a ≤ k ∧ k ≤ j ⟶
semantics_mltl (drop k π) ψ))"
using * h1 by blast
then have "∃j. a ≤ j ∧ j ≤ b-1 ∧ (semantics_mltl (drop j π) φ ∧ (∀k. a ≤ k ∧ k ≤ j ⟶ semantics_mltl (drop k π) ψ))"
using relase_unfold
by metis
then have "∀i. a ≤ i ∧ i ≤ b ⟶
(semantics_mltl (drop i π) ψ ∨
(∃j. a ≤ j ∧ j < i ∧ semantics_mltl (drop j π) φ))"
by (metis linorder_not_less)
then have "∀i. (i ≥ a ∧ i ≤ b) ⟶ (semantics_mltl (drop i π) ψ ∨
¬ (∀j. a ≤ j ∧ j < i ⟶ ¬ semantics_mltl (drop j π) φ))"
by blast
then have "∀i. (i ≥ a ∧ i ≤ b) ⟶ ¬ (¬ semantics_mltl (drop i π) ψ ∧
(∀j. a ≤ j ∧ j < i ⟶ ¬ semantics_mltl (drop j π) φ))"
by blast
then have "¬ ((∃i::nat. (i ≥ a ∧ i ≤ b) ∧ (¬ (semantics_mltl (drop i π) ψ) ∧ (∀j. j ≥ a ∧ j<i ⟶ ¬ (semantics_mltl (drop j π ) φ)))))"
by blast
then have "¬ (a ≤ b ∧ length π > a ∧ (∃i::nat. (i ≥ a ∧ i ≤ b) ∧ (¬ (semantics_mltl (drop i π) ψ) ∧ (∀j. j ≥ a ∧ j<i ⟶ ¬ (semantics_mltl (drop j π ) φ)))))"
using * by blast
then have ?thesis
by auto
}
ultimately show ?thesis
using linorder_not_less
by (smt (verit) relase_unfold semantics_mltl.simps(4) semantics_mltl.simps(9))
qed
lemma release_until_dual2:
fixes a b::"nat"
assumes a_leq_b: "a ≤ b"
assumes "π ⊨⇩m (Not⇩m ((Not⇩m φ) U⇩m [a,b] (Not⇩m ψ)))"
shows "semantics_mltl π (φ R⇩m [a,b] ψ)"
proof -
have unfold_not_until_not: " ¬ (a ≤ b ∧ length π > a ∧ (∃i::nat. (i ≥ a ∧ i ≤ b) ∧ (¬ (semantics_mltl (drop i π) ψ) ∧ (∀j. j ≥ a ∧ j<i ⟶ ¬ (semantics_mltl (drop j π ) φ)))))"
using assms by auto
have not_until_not_unfold: "(a ≤ b ∧ a < length π) ⟶ (π ⊨⇩m (Not⇩m ((Not⇩m φ) U⇩m [a,b] (Not⇩m ψ))) ⟷
(∀i. a ≤ i ∧ i ≤ b ⟶
semantics_mltl (drop i π) ψ ∨
(∃j. a ≤ j ∧ j < i ∧ semantics_mltl (drop j π) φ)))"
by auto
{assume *: "length π ≤ a"
then have ?thesis
using assms semantics_mltl.simps(10)
by blast
} moreover {assume *: "∀s. (a ≤ s ∧ s ≤ b) ⟶ semantics_mltl (drop s π) ψ"
then have ?thesis
by (simp add: assms(1))
} moreover {assume *: "(a ≤ b ∧ a < length π) ∧ (∃s. (a ≤ s ∧ s ≤ b) ∧ ¬ (semantics_mltl (drop s π) ψ))"
then have not_until_not: "(∀i. a ≤ i ∧ i ≤ b ⟶
semantics_mltl (drop i π) ψ ∨
(∃j. a ≤ j ∧ j < i ∧ semantics_mltl (drop j π) φ))"
using not_until_not_unfold assms
by blast
have least_prop: "(∃s. (a ≤ s ∧ s ≤ b) ∧ f s π ψ ∧
(∀k. a ≤ k ∧ k < s ⟶ ¬ (f k π ψ))
)" if f_prop: "(∃s. (a ≤ s ∧ s ≤ b) ∧ f s π ψ)" for f::"nat ⇒ 'a set list ⇒ 'a mltl ⇒ bool"
proof -
have "∃q. q = (LEAST p. (a ≤ p ∧ p ≤ b) ∧ f p π ψ)"
by simp
then obtain q where q_prop: "q = (LEAST p. (a ≤ p ∧ p ≤ b) ∧ f p π ψ)"
by auto
then have least1: "(a ≤ q ∧ q ≤ b) ∧ f q π ψ"
using f_prop
by (smt (verit) LeastI)
have least2: "(∀k. a ≤ k ∧ k < q ⟶ ¬ (f k π ψ))"
using q_prop
using least1 not_less_Least by fastforce
show ?thesis using least1 least2 by blast
qed
have "∃i1. a ≤ i1 ∧ i1 ≤ b ∧ ¬ (semantics_mltl (drop i1 π) ψ) ∧ (∀k. (a ≤ k ∧ k ≤ i1-1) ⟶ (semantics_mltl (drop k π) ψ))"
using * least_prop[of "λ s π ψ. ¬ (semantics_mltl (drop s π) ψ)"]
by (metis add_diff_inverse_nat gr_implies_not0 le_imp_less_Suc less_one plus_1_eq_Suc unfold_not_until_not)
then obtain i1 where i1_prop: "a ≤ i1 ∧ i1 ≤ b ∧ ¬ (semantics_mltl (drop i1 π) ψ) ∧ (∀k. (a ≤ k ∧ k ≤ i1-1) ⟶ (semantics_mltl (drop k π) ψ))"
by auto
have "semantics_mltl (drop i1 π) ψ ∨
(∃j≥a. j < i1 ∧ semantics_mltl (drop j π) φ)"
using not_until_not i1_prop by blast
then have "(semantics_mltl (drop i1 π) ψ) ∨ (∃t. a ≤ t ∧ t ≤ i1-1 ∧ (semantics_mltl (drop t π) φ))"
using * i1_prop
using not_less_eq by fastforce
then have "(∃t. a ≤ t ∧ t ≤ i1-1 ∧ (semantics_mltl (drop t π) φ))"
by (smt (verit, ccfv_threshold) "*" i1_prop less_imp_le_nat nle_le not_until_not order_le_less_trans)
then obtain t where t_prop: "a ≤ t ∧ t ≤ i1-1 ∧ semantics_mltl (drop t π) φ"
by auto
have "∀k. a ≤ k ∧ k ≤ i1-1 ⟶ (semantics_mltl (drop k π) ψ )"
using i1_prop by blast
then have "∀k. a ≤ k ∧ k ≤ t ⟶ (semantics_mltl (drop k π) ψ )"
using t_prop by auto
then have "∃j. a ≤ j ∧ j ≤ (b-1) ∧ (semantics_mltl (drop j π) φ)
∧ (∀k. a ≤ k ∧k ≤ j ⟶ (semantics_mltl (drop k π) ψ))"
by (meson diff_le_mono i1_prop le_trans t_prop)
then have ?thesis
using semantics_mltl.simps(10) a_leq_b
by blast
}
ultimately show ?thesis
using assms(1) linorder_not_less by blast
qed
lemma release_until_dual:
fixes a b::"nat"
assumes a_leq_b: "a ≤ b"
shows "(φ R⇩m [a,b] ψ) ≡⇩m (Not⇩m ((Not⇩m φ) U⇩m [a,b] (Not⇩m ψ)))"
using release_until_dual1 release_until_dual2
using assms unfolding semantic_equiv_def by metis
lemma until_release_dual:
fixes a b::"nat"
assumes a_leq_b: "a ≤ b"
shows "(φ U⇩m [a,b] ψ) ≡⇩m (Not⇩m ((Not⇩m φ) R⇩m [a,b] (Not⇩m ψ)))"
proof-
have release_until_dual_alternate: "(Not⇩m (φ R⇩m [a,b] ψ)) ≡⇩m ((Not⇩m φ) U⇩m [a,b] (Not⇩m ψ))"
using release_until_dual
using assms semantics_mltl.simps(4) unfolding semantic_equiv_def by metis
have not_not_until: "(φ U⇩m [a,b] ψ) ≡⇩m ((Not⇩m (Not⇩m φ)) U⇩m [a,b] (Not⇩m (Not⇩m ψ)))"
using assms not_not_equiv using semantics_mltl.simps(9)
by (simp add: semantic_equiv_def)
have "(Not⇩m ((Not⇩m φ) R⇩m [a,b] (Not⇩m ψ))) ≡⇩m ((Not⇩m (Not⇩m φ)) U⇩m [a,b] (Not⇩m (Not⇩m ψ)))"
using assms release_until_dual semantics_mltl.simps(4) unfolding semantic_equiv_def by metis
then show ?thesis using not_not_until
unfolding semantic_equiv_def
by blast
qed
subsection "Additional Basic Properties"
lemma release_and_distribute:
fixes a b ::"nat"
assumes "a ≤ b"
shows "(φ R⇩m [a,b] (α And⇩m β)) ≡⇩m
((φ R⇩m [a,b] α) And⇩m (φ R⇩m [a,b] β))"
proof-
let ?lhs = "(φ R⇩m [a,b] (α And⇩m β))"
let ?rhs = "((φ R⇩m [a,b] α) And⇩m (φ R⇩m [a,b] β))"
let ?neg = "Not⇩m ((Not⇩m φ) U⇩m [a,b] (Not⇩m (α And⇩m β)))"
have eq_lhs: "semantic_equiv ?lhs ?neg"
using until_release_dual release_until_dual until_or_distribute
by (smt (verit) assms release_until_dual1 semantic_equiv_def)
let ?neg1 = "Not⇩m ((Not⇩m φ) U⇩m [a,b] ((Not⇩m α) Or⇩m (Not⇩m β)))"
have eq_neg1: "semantic_equiv ?neg ?neg1"
unfolding semantic_equiv_def semantic_equiv_def by auto
let ?neg2 = "Not⇩m (((Not⇩m φ) U⇩m [a,b] (Not_mltl α)) Or⇩m ((Not⇩m φ) U⇩m [a,b] (Not_mltl β)))"
have eq_neg2: "semantic_equiv ?neg1 ?neg2"
unfolding semantic_equiv_def by auto
let ?neg3 = "((φ R⇩m [a,b] α) And⇩m (φ R⇩m [a,b] β))"
have eq_neg3: "semantic_equiv ?neg2 ?neg3"
unfolding semantic_equiv_def using assms
by (metis release_until_dual1 release_until_dual2 semantics_mltl.simps(4) semantics_mltl.simps(5) semantics_mltl.simps(6))
have eq_rhs: "semantic_equiv ?rhs ?neg"
using eq_neg1 eq_neg2 eq_neg3
by (meson semantic_equiv_def)
show ?thesis using eq_rhs eq_lhs unfolding semantic_equiv_def by meson
qed
subsection ‹NNF Transformation and Properties ›
fun convert_nnf:: "'a mltl ⇒ 'a mltl"
where "convert_nnf True⇩m = True⇩m"
| "convert_nnf False⇩m = False⇩m"
| "convert_nnf Prop⇩m (p) = Prop⇩m (p)"
| "convert_nnf (φ And⇩m ψ) = ((convert_nnf φ) And⇩m (convert_nnf ψ))"
| "convert_nnf (φ Or⇩m ψ) = ((convert_nnf φ) Or⇩m (convert_nnf ψ))"
| "convert_nnf (F⇩m [a,b] φ) = (F⇩m [a,b] (convert_nnf φ))"
| "convert_nnf (G⇩m [a,b] φ) = (G⇩m [a,b] (convert_nnf φ))"
| "convert_nnf (φ U⇩m [a,b] ψ) = ((convert_nnf φ) U⇩m [a,b] (convert_nnf ψ))"
| "convert_nnf (φ R⇩m [a,b] ψ) = ((convert_nnf φ) R⇩m [a,b] (convert_nnf ψ))"
| "convert_nnf (Not⇩m True⇩m) = False⇩m"
| "convert_nnf (Not⇩m False⇩m) = True⇩m"
| "convert_nnf (Not⇩m Prop⇩m (p)) = (Not⇩m Prop⇩m (p))"
| "convert_nnf (Not⇩m (Not⇩m φ)) = convert_nnf φ"
| "convert_nnf (Not⇩m (φ And⇩m ψ)) = ((convert_nnf (Not⇩m φ)) Or⇩m (convert_nnf (Not⇩m ψ)))"
| "convert_nnf (Not⇩m (φ Or⇩m ψ)) = ((convert_nnf (Not⇩m φ)) And⇩m (convert_nnf (Not⇩m ψ)))"
| "convert_nnf (Not⇩m (F⇩m [a,b] φ)) = (G⇩m [a,b] (convert_nnf (Not⇩m φ)))"
| "convert_nnf (Not⇩m (G⇩m [a,b] φ)) = (F⇩m [a,b] (convert_nnf (Not⇩m φ)))"
| "convert_nnf (Not⇩m (φ U⇩m [a,b] ψ)) = ((convert_nnf (Not⇩m φ)) R⇩m [a,b] (convert_nnf (Not⇩m ψ)))"
| "convert_nnf (Not⇩m (φ R⇩m [a,b] ψ)) = ((convert_nnf (Not⇩m φ)) U⇩m [a,b] (convert_nnf (Not⇩m ψ)))"
lemma convert_nnf_preserves_semantics:
assumes "intervals_welldef φ"
shows "(π ⊨⇩m (convert_nnf φ)) ⟷ (π ⊨⇩m φ)"
using assms
proof (induct "depth_mltl φ" arbitrary:φ π rule:less_induct)
case less
then show ?case
proof (cases φ)
case True_mltl
then show ?thesis by simp
next
case False_mltl
then show ?thesis by simp
next
case (Prop_mltl x)
then show ?thesis by simp
next
case (Not_mltl φ1)
then have phi_is: "φ = Not⇩m φ1"
by auto
then show ?thesis
proof (cases φ1)
case True_mltl
then show ?thesis using Not_mltl
by simp
next
case False_mltl
then show ?thesis using Not_mltl
by simp
next
case (Prop_mltl p)
then show ?thesis using Not_mltl
by simp
next
case (Not_mltl φ2)
then show ?thesis using phi_is less
by auto
next
case (And_mltl φ2 φ3)
then show ?thesis using phi_is less
by auto
next
case (Or_mltl φ2 φ3)
then show ?thesis using phi_is less
by auto
next
case (Future_mltl a b φ2)
then have *: "a ≤ b" using less(2)
phi_is by simp
have "semantics_mltl π (convert_nnf φ) = semantics_mltl π (Global_mltl a b (convert_nnf (Not⇩m φ2)))"
using Future_mltl phi_is by simp
then have semantics_unfold: "semantics_mltl π (convert_nnf φ) = (a ≤ b ∧ (length π ≤ a ∨ (∀i::nat. (i ≥ a ∧ i ≤ b) ⟶ semantics_mltl (drop i π) (convert_nnf (Not⇩m φ2)))))"
by auto
have "intervals_welldef (Not⇩m φ2)"
using less(2) Future_mltl phi_is by simp
then have "semantics_mltl (drop i π) (convert_nnf (Not⇩m φ2)) = semantics_mltl (drop i π) (Not⇩m φ2)" for i
using less(1)[of "Not⇩m φ2" "(drop i π)"] phi_is Future_mltl
by auto
then have semantics_unfold1: "semantics_mltl π (convert_nnf φ) = (a ≤ b ∧ (length π ≤ a ∨ (∀i::nat. (i ≥ a ∧ i ≤ b) ⟶ semantics_mltl (drop i π) (Not⇩m φ2))))"
using semantics_unfold by auto
have "semantics_mltl π φ = (¬ (semantics_mltl π (Future_mltl a b φ2)))"
using phi_is Future_mltl by simp
then show ?thesis using semantics_unfold1 *
by auto
next
case (Global_mltl a b φ2)
then have *: "a ≤ b" using less(2)
phi_is by simp
have "semantics_mltl π (convert_nnf φ) = semantics_mltl π (Future_mltl a b (convert_nnf (Not⇩m φ2)))"
using Global_mltl phi_is by simp
then have semantics_unfold: "semantics_mltl π (convert_nnf φ) = (a ≤ b ∧ length π > a ∧ (∃i::nat. (i ≥ a ∧ i ≤ b) ∧ semantics_mltl (drop i π) (convert_nnf (Not⇩m φ2))))"
by auto
have "intervals_welldef (Not⇩m φ2)"
using less(2) Global_mltl phi_is by simp
then have "semantics_mltl (drop i π) (convert_nnf (Not⇩m φ2)) = semantics_mltl (drop i π) (Not⇩m φ2)" for i
using less(1)[of "Not⇩m φ2" "(drop i π)"] phi_is Global_mltl
by auto
then have semantics_unfold1: "semantics_mltl π (convert_nnf φ) = (a ≤ b ∧ length π > a ∧ (∃i::nat. (i ≥ a ∧ i ≤ b) ∧ semantics_mltl (drop i π) (Not⇩m φ2)))"
using semantics_unfold by auto
have "semantics_mltl π φ = (¬ (semantics_mltl π (Global_mltl a b φ2)))"
using phi_is Global_mltl by simp
then show ?thesis using semantics_unfold1 *
by auto
next
case (Until_mltl φ2 a b φ3)
then have *: "a ≤ b" using less(2)
phi_is by simp
have "semantics_mltl π (convert_nnf φ) = semantics_mltl π (Release_mltl (convert_nnf (Not⇩m φ2)) a b (convert_nnf (Not⇩m φ3)))"
using Until_mltl phi_is by simp
then have semantics_unfold: "semantics_mltl π (convert_nnf φ) = (a ≤ b ∧ (length π ≤ a ∨ (∀i::nat. (i ≥ a ∧ i ≤ b) ⟶ ((semantics_mltl (drop i π) (convert_nnf (Not⇩m φ3))))) ∨ (∃j. j ≥ a ∧ j ≤ b-1 ∧ semantics_mltl (drop j π) (convert_nnf (Not⇩m φ2)) ∧ (∀k. a ≤ k ∧ k ≤ j ⟶ semantics_mltl (drop k π) (convert_nnf (Not⇩m φ3))))))"
by auto
have phi3_ind_h: "semantics_mltl (drop i π) (convert_nnf (Not⇩m φ3)) = semantics_mltl (drop i π) (Not⇩m φ3)" for i
using less(1)[of "Not⇩m φ3" "(drop i π)"] phi_is Until_mltl
using less.prems by force
have phi2_ind_h: "semantics_mltl (drop i π) (convert_nnf (Not⇩m φ2)) = semantics_mltl (drop i π) (Not⇩m φ2)" for i
using less(1)[of "Not⇩m φ2" "(drop i π)"] phi_is Until_mltl
using less.prems by force
have semantics_unfold1: "semantics_mltl π (convert_nnf φ) = (length π ≤ a ∨ (∀i::nat. (i ≥ a ∧ i ≤ b) ⟶ ((semantics_mltl (drop i π) (Not⇩m φ3)))) ∨ (∃j. j ≥ a ∧ j ≤ b-1 ∧ semantics_mltl (drop j π) (Not⇩m φ2) ∧ (∀k. a ≤ k ∧ k ≤ j ⟶ semantics_mltl (drop k π) (Not⇩m φ3))))"
using * phi3_ind_h phi2_ind_h semantics_unfold by auto
have "semantics_mltl π φ = semantics_mltl π (Release_mltl (Not⇩m φ2) a b (Not⇩m φ3))"
using Until_mltl phi_is until_release_dual[OF *]
using semantics_mltl.simps(4)
using semantic_equiv_def by blast
then show ?thesis using semantics_unfold1 *
by auto
next
case (Release_mltl φ2 a b φ3)
then have *: "a ≤ b" using less(2)
phi_is by simp
have "semantics_mltl π (convert_nnf φ) = semantics_mltl π (Until_mltl (convert_nnf (Not⇩m φ2)) a b (convert_nnf (Not⇩m φ3)))"
using Release_mltl phi_is by simp
then have semantics_unfold: "semantics_mltl π (convert_nnf φ) = (a ≤ b ∧ length π > a ∧ (∃i::nat. (i ≥ a ∧ i ≤ b) ∧ (semantics_mltl (drop i π) (convert_nnf (Not⇩m φ3)) ∧ (∀j. j ≥ a ∧ j<i ⟶ semantics_mltl (drop j π ) (convert_nnf (Not⇩m φ2))))))"
by auto
have phi3_ind_h: "semantics_mltl (drop i π) (convert_nnf (Not⇩m φ3)) = semantics_mltl (drop i π) (Not⇩m φ3)" for i
using less(1)[of "Not⇩m φ3" "(drop i π)"] phi_is Release_mltl
using less.prems by force
have phi2_ind_h: "semantics_mltl (drop i π) (convert_nnf (Not⇩m φ2)) = semantics_mltl (drop i π) (Not⇩m φ2)" for i
using less(1)[of "Not⇩m φ2" "(drop i π)"] phi_is Release_mltl
using less.prems by force
have semantics_unfold1: "semantics_mltl π (convert_nnf φ) = (length π > a ∧ (∃i::nat. (i ≥ a ∧ i ≤ b) ∧ (semantics_mltl (drop i π) (Not⇩m φ3) ∧ (∀j. j ≥ a ∧ j<i ⟶ semantics_mltl (drop j π) (Not⇩m φ2)))))"
using * phi3_ind_h phi2_ind_h semantics_unfold by auto
have "semantics_mltl π φ = semantics_mltl π (Until_mltl (Not⇩m φ2) a b (Not⇩m φ3))"
using Release_mltl phi_is release_until_dual[OF *]
using semantics_mltl.simps(4) unfolding semantic_equiv_def by metis
then show ?thesis using semantics_unfold1 *
by auto
qed
next
case (And_mltl φ1 φ2)
then show ?thesis using less by simp
next
case (Or_mltl φ1 φ2)
then show ?thesis using less by simp
next
case (Future_mltl a b φ1)
then have "intervals_welldef φ1"
using less(2) by simp
then have ind_h: "semantics_mltl (drop i π) (convert_nnf φ1) = semantics_mltl (drop i π) φ1" for i
using Future_mltl less(1)[of φ1 "(drop i π)"]
by auto
have unfold_future: "semantics_mltl π (convert_nnf (Future_mltl a b φ1)) = semantics_mltl π (Future_mltl a b (convert_nnf φ1))"
by simp
moreover then have unfold_future_semantics: "... = (a ≤ b ∧ length π > a ∧ (∃i::nat. (i ≥ a ∧ i ≤ b) ∧ semantics_mltl (drop i π) (convert_nnf φ1)))"
by simp
moreover then have "... = (a ≤ b ∧ length π > a ∧ (∃i::nat. (i ≥ a ∧ i ≤ b) ∧ semantics_mltl (drop i π) φ1))"
using ind_h
by auto
ultimately show ?thesis using Future_mltl
by simp
next
case (Global_mltl a b φ1)
then have "intervals_welldef φ1"
using less(2) by simp
then have ind_h: "semantics_mltl (drop i π) (convert_nnf φ1) = semantics_mltl (drop i π) φ1" for i
using Global_mltl less(1)[of φ1 "(drop i π)"]
by auto
have unfold_future: "semantics_mltl π (convert_nnf (Global_mltl a b φ1)) = semantics_mltl π (Global_mltl a b (convert_nnf φ1))"
by simp
moreover then have unfold_future_semantics: "... = (a ≤ b ∧ (length π ≤ a ∨ (∀i::nat. (i ≥ a ∧ i ≤ b) ⟶ semantics_mltl (drop i π) (convert_nnf φ1))))"
by simp
moreover then have "... = (a ≤ b ∧ (length π ≤ a ∨ (∀i::nat. (i ≥ a ∧ i ≤ b) ⟶ semantics_mltl (drop i π) φ1)))"
using ind_h
by auto
ultimately show ?thesis using Global_mltl
by simp
next
case (Until_mltl φ1 a b φ2)
then have *: "a ≤ b" using less(2)
Until_mltl by simp
have semantics_unfold: "semantics_mltl π (convert_nnf φ) = (a ≤ b ∧ length π > a ∧ (∃i::nat. (i ≥ a ∧ i ≤ b) ∧ (semantics_mltl (drop i π) (convert_nnf φ2) ∧ (∀j. j ≥ a ∧ j<i ⟶ semantics_mltl (drop j π ) (convert_nnf φ1)))))"
using Until_mltl by auto
have phi3_ind_h: "semantics_mltl (drop i π) (convert_nnf φ1) = semantics_mltl (drop i π) φ1" for i
using less(1)[of φ1 "(drop i π)"] Until_mltl less.prems
by force
have phi2_ind_h: "semantics_mltl (drop i π) (convert_nnf φ2) = semantics_mltl (drop i π) φ2" for i
using less(1)[of φ2 "(drop i π)"] Until_mltl less.prems
by force
have semantics_unfold1: "semantics_mltl π (convert_nnf φ) = (length π > a ∧ (∃i::nat. (i ≥ a ∧ i ≤ b) ∧ (semantics_mltl (drop i π) φ2 ∧ (∀j. j ≥ a ∧ j<i ⟶ semantics_mltl (drop j π ) φ1))))"
using * phi3_ind_h phi2_ind_h semantics_unfold
by auto
then show ?thesis using semantics_unfold1 * Until_mltl
by auto
next
case (Release_mltl φ1 a b φ2)
then have *: "a ≤ b" using less(2)
Release_mltl by simp
have semantics_unfold: "semantics_mltl π (convert_nnf φ) = (a ≤ b ∧ (length π ≤ a ∨ (∀i::nat. (i ≥ a ∧ i ≤ b) ⟶ ((semantics_mltl (drop i π) (convert_nnf φ2)))) ∨ (∃j. j ≥ a ∧ j ≤ b-1 ∧ semantics_mltl (drop j π) (convert_nnf φ1) ∧ (∀k. a ≤ k ∧ k ≤ j ⟶ semantics_mltl (drop k π) (convert_nnf φ2)))))"
using Release_mltl by auto
have phi3_ind_h: "semantics_mltl (drop i π) (convert_nnf φ1) = semantics_mltl (drop i π) φ1" for i
using less(1)[of φ1 "(drop i π)"] Release_mltl less.prems
by force
have phi2_ind_h: "semantics_mltl (drop i π) (convert_nnf φ2) = semantics_mltl (drop i π) φ2" for i
using less(1)[of φ2 "(drop i π)"] Release_mltl less.prems
by force
have semantics_unfold1: "semantics_mltl π (convert_nnf φ) = (length π ≤ a ∨ (∀i::nat. (i ≥ a ∧ i ≤ b) ⟶ ((semantics_mltl (drop i π) φ2))) ∨ (∃j. j ≥ a ∧ j ≤ b-1 ∧ semantics_mltl (drop j π) φ1 ∧ (∀k. a ≤ k ∧ k ≤ j ⟶ semantics_mltl (drop k π) φ2)))"
using * phi3_ind_h phi2_ind_h semantics_unfold
by auto
then show ?thesis using semantics_unfold1 * Release_mltl
by auto
qed
qed
lemma convert_nnf_form_Not_Implies_Prop:
assumes "Not⇩m F = convert_nnf init_F"
shows "∃p. F = Prop⇩m (p)"
using assms
proof (induct "depth_mltl init_F" arbitrary: init_F rule: less_induct)
case less
then have ind_h1: "⋀G. depth_mltl G < depth_mltl init_F ⟹
Not_mltl F = convert_nnf G ⟹ ∃p. F = Prop_mltl p"
by auto
have not: "Not_mltl F = convert_nnf init_F" using less
by auto
then show ?case proof (cases init_F)
case True_mltl
then show ?thesis using ind_h1 not by auto
next
case False_mltl
then show ?thesis using ind_h1 not by auto
next
case (Prop_mltl p)
then show ?thesis using ind_h1 not by auto
next
case (Not_mltl φ)
then have init_F_is: "init_F = Not⇩m φ"
by auto
then show ?thesis proof (cases φ)
case True_mltl
then show ?thesis using ind_h1 not init_F_is by auto
next
case False_mltl
then show ?thesis using ind_h1 not init_F_is by auto
next
case (Prop_mltl p)
then show ?thesis using ind_h1 not init_F_is by auto
next
case (Not_mltl φ)
then have not_convert: "Not_mltl F = convert_nnf φ" using not init_F_is
by auto
have depth: "depth_mltl φ < depth_mltl init_F"
using Not_mltl init_F_is by auto
then show ?thesis using ind_h1[OF depth not_convert] by auto
next
case (And_mltl φ ψ)
then show ?thesis using ind_h1 not init_F_is by auto
next
case (Or_mltl φ ψ)
then show ?thesis using ind_h1 not init_F_is by auto
next
case (Future_mltl a b φ)
then show ?thesis using ind_h1 not init_F_is by auto
next
case (Global_mltl a b φ)
then show ?thesis using ind_h1 not init_F_is by auto
next
case (Until_mltl φ a b ψ)
then show ?thesis using ind_h1 not init_F_is by auto
next
case (Release_mltl φ a b ψ)
then show ?thesis using ind_h1 not init_F_is by auto
qed
next
case (And_mltl φ ψ)
then show ?thesis using ind_h1 not by auto
next
case (Or_mltl φ ψ)
then show ?thesis using ind_h1 not by auto
next
case (Future_mltl a b φ)
then show ?thesis using ind_h1 not by auto
next
case (Global_mltl a b φ)
then show ?thesis using ind_h1 not by auto
next
case (Until_mltl φ a b ψ)
then show ?thesis using ind_h1 not by auto
next
case (Release_mltl φ a b ψ)
then show ?thesis using ind_h1 not by auto
qed
qed
lemma convert_nnf_convert_nnf:
shows "convert_nnf (convert_nnf F) = convert_nnf F"
proof (induction "depth_mltl F" arbitrary: F rule: less_induct)
case less
have not_case: "(⋀F. depth_mltl F < Suc (depth_mltl G) ⟹
convert_nnf (convert_nnf F) = convert_nnf F) ⟹
F = Not_mltl G ⟹
convert_nnf (convert_nnf (Not_mltl G)) = convert_nnf (Not_mltl G)" for "G"
proof -
assume ind_h: "(⋀F. depth_mltl F < Suc (depth_mltl G) ⟹
convert_nnf (convert_nnf F) = convert_nnf F)"
assume F_is: "F = Not_mltl G"
show ?thesis using less F_is apply (cases G) by simp_all
qed
show ?case using less apply (cases F) apply simp_all using not_case
by auto
qed
lemma nnf_subformulas:
assumes "F = convert_nnf init_F"
assumes "G ∈ subformulas F"
shows "∃ init_G. G = convert_nnf init_G"
using assms proof (induct "depth_mltl init_F" arbitrary: init_F F G rule: less_induct)
case less
then show ?case proof (cases init_F)
case True_mltl
then show ?thesis using less by simp
next
case False_mltl
then show ?thesis using less by simp
next
case (Prop_mltl p)
then show ?thesis using less by simp
next
case (Not_mltl φ)
then have init_is: "init_F = Not⇩m φ"
by auto
then show ?thesis proof (cases φ)
case True_mltl
then show ?thesis using less init_is
by auto
next
case False_mltl
then show ?thesis using less init_is
by auto
next
case (Prop_mltl p)
then have "init_F = (Not_mltl Prop⇩m (p))"
using init_is by auto
then have "G = Prop_mltl p"
using less by simp
then have "G = convert_nnf Prop⇩m (p)"
by auto
then show ?thesis by blast
next
case (Not_mltl ψ)
then have init_is2: "init_F = (Not_mltl (Not_mltl ψ))"
using init_is by auto
then have F_is: "F = convert_nnf ψ"
using less by auto
then show ?thesis using less.hyps[OF _ F_is] init_is2 less(3)
by simp
next
case (And_mltl ψ1 ψ2)
then have init_is2: "init_F = (Not_mltl (And_mltl ψ1 ψ2))"
using init_is by auto
then have F_is: "F = (Or_mltl (convert_nnf (Not_mltl ψ1)) (convert_nnf (Not_mltl ψ2)))"
using less by auto
have depth1: "depth_mltl (Not_mltl ψ1) < depth_mltl init_F"
using init_is2
by simp
have depth2: "depth_mltl (Not_mltl ψ2) < depth_mltl init_F"
using init_is2
by simp
have G_inset: "G ∈ {(convert_nnf (Not_mltl ψ1)), (convert_nnf (Not_mltl ψ2))}
∪ subformulas (convert_nnf (Not_mltl ψ1)) ∪ subformulas (convert_nnf (Not_mltl ψ2))"
using F_is less(3) by auto
then show ?thesis using less.hyps[OF depth1, of "convert_nnf (Not_mltl ψ1)"] less.hyps[OF depth2, of "convert_nnf (Not_mltl ψ2)"]
G_inset by blast
next
case (Or_mltl ψ1 ψ2)
then have init_is2: "init_F = (Not_mltl (Or_mltl ψ1 ψ2))"
using init_is by auto
then have F_is: "F = (And_mltl (convert_nnf (Not_mltl ψ1)) (convert_nnf (Not_mltl ψ2)))"
using less by auto
have depth1: "depth_mltl (Not_mltl ψ1) < depth_mltl init_F"
using init_is2
by simp
have depth2: "depth_mltl (Not_mltl ψ2) < depth_mltl init_F"
using init_is2
by simp
have G_inset: "G ∈ {(convert_nnf (Not_mltl ψ1)), (convert_nnf (Not_mltl ψ2))}
∪ subformulas (convert_nnf (Not_mltl ψ1)) ∪ subformulas (convert_nnf (Not_mltl ψ2))"
using F_is less(3) by auto
then show ?thesis using less.hyps[OF depth1, of "convert_nnf (Not_mltl ψ1)"] less.hyps[OF depth2, of "convert_nnf (Not_mltl ψ2)"]
G_inset by blast
next
case (Future_mltl a b ψ)
then have init_is2: "init_F = (Not_mltl (Future_mltl a b ψ))"
using init_is by auto
then have F_is: "F = (Global_mltl a b (convert_nnf (Not_mltl ψ)))"
using less by auto
have depth1: "depth_mltl (Not_mltl ψ) < depth_mltl init_F"
using init_is2
by simp
have G_inset: "G ∈ {(convert_nnf (Not_mltl ψ))}
∪ subformulas (convert_nnf (Not_mltl ψ))"
using F_is less(3) by auto
then show ?thesis using less.hyps[OF depth1, of "convert_nnf (Not_mltl ψ)"]
G_inset by blast
next
case (Global_mltl a b ψ)
then have init_is2: "init_F = (Not_mltl (Global_mltl a b ψ))"
using init_is by auto
then have F_is: "F = (Future_mltl a b (convert_nnf (Not_mltl ψ)))"
using less by auto
have depth1: "depth_mltl (Not_mltl ψ) < depth_mltl init_F"
using init_is2
by simp
have G_inset: "G ∈ {(convert_nnf (Not_mltl ψ))}
∪ subformulas (convert_nnf (Not_mltl ψ))"
using F_is less(3) by auto
then show ?thesis using less.hyps[OF depth1, of "convert_nnf (Not_mltl ψ)"]
G_inset by blast
next
case (Until_mltl ψ1 a b ψ2)
then have init_is2: "init_F = (Not_mltl (Until_mltl ψ1 a b ψ2))"
using init_is by auto
then have F_is: "F = (Release_mltl (convert_nnf (Not_mltl ψ1)) a b (convert_nnf (Not_mltl ψ2)))"
using less by auto
have depth1: "depth_mltl (Not_mltl ψ1) < depth_mltl init_F"
using init_is2
by simp
have depth2: "depth_mltl (Not_mltl ψ2) < depth_mltl init_F"
using init_is2
by simp
have G_inset: "G ∈ {(convert_nnf (Not_mltl ψ1)), (convert_nnf (Not_mltl ψ2))}
∪ subformulas (convert_nnf (Not_mltl ψ1)) ∪ subformulas (convert_nnf (Not_mltl ψ2))"
using F_is less(3) by auto
then show ?thesis using less.hyps[OF depth1, of "convert_nnf (Not_mltl ψ1)"] less.hyps[OF depth2, of "convert_nnf (Not_mltl ψ2)"]
G_inset by blast
next
case (Release_mltl ψ1 a b ψ2)
then have init_is2: "init_F = (Not_mltl (Release_mltl ψ1 a b ψ2))"
using init_is by auto
then have F_is: "F = (Until_mltl (convert_nnf (Not_mltl ψ1)) a b (convert_nnf (Not_mltl ψ2)))"
using less by auto
have depth1: "depth_mltl (Not_mltl ψ1) < depth_mltl init_F"
using init_is2
by simp
have depth2: "depth_mltl (Not_mltl ψ2) < depth_mltl init_F"
using init_is2
by simp
have G_inset: "G ∈ {(convert_nnf (Not_mltl ψ1)), (convert_nnf (Not_mltl ψ2))}
∪ subformulas (convert_nnf (Not_mltl ψ1)) ∪ subformulas (convert_nnf (Not_mltl ψ2))"
using F_is less(3) by auto
then show ?thesis using less.hyps[OF depth1, of "convert_nnf (Not_mltl ψ1)"] less.hyps[OF depth2, of "convert_nnf (Not_mltl ψ2)"]
G_inset by blast
qed
next
case (And_mltl φ1 φ2)
then have F_is: "F = And_mltl (convert_nnf φ1) (convert_nnf φ2)"
using less by auto
then have G_inset: "G ∈ {(convert_nnf φ1), (convert_nnf φ2)} ∪ subformulas (convert_nnf φ1) ∪
subformulas (convert_nnf φ2)" using less(3) by simp
have depth_phi1: "depth_mltl φ1 < depth_mltl init_F"
using less And_mltl by simp
have depth_phi2: "depth_mltl φ2 < depth_mltl init_F"
using less And_mltl by simp
then show ?thesis using less.hyps[OF depth_phi1, of "convert_nnf φ1"] using less.hyps[OF depth_phi2, of "convert_nnf φ2"]
G_inset by blast
next
case (Or_mltl φ1 φ2)
then have F_is: "F = Or_mltl (convert_nnf φ1) (convert_nnf φ2)"
using less by auto
then have G_inset: "G ∈ {(convert_nnf φ1), (convert_nnf φ2)} ∪ subformulas (convert_nnf φ1) ∪
subformulas (convert_nnf φ2)" using less(3) by simp
have depth_phi1: "depth_mltl φ1 < depth_mltl init_F"
using less Or_mltl by simp
have depth_phi2: "depth_mltl φ2 < depth_mltl init_F"
using less Or_mltl by simp
then show ?thesis using less.hyps[OF depth_phi1, of "convert_nnf φ1"] using less.hyps[OF depth_phi2, of "convert_nnf φ2"]
G_inset by blast
next
case (Future_mltl a b φ)
then have F_is: "F = Future_mltl a b (convert_nnf φ)"
using less by auto
then have G_inset: "G ∈ {(convert_nnf φ)} ∪ subformulas (convert_nnf φ)"
using less(3) by simp
have depth_phi1: "depth_mltl φ < depth_mltl init_F"
using less Future_mltl by simp
then show ?thesis using less.hyps[OF depth_phi1, of "convert_nnf φ"]
G_inset by blast
next
case (Global_mltl a b φ)
then have F_is: "F = Global_mltl a b (convert_nnf φ)"
using less by auto
then have G_inset: "G ∈ {(convert_nnf φ)} ∪ subformulas (convert_nnf φ)"
using less(3) by simp
have depth_phi1: "depth_mltl φ < depth_mltl init_F"
using less Global_mltl by simp
then show ?thesis using less.hyps[OF depth_phi1, of "convert_nnf φ"]
G_inset by blast
next
case (Until_mltl φ1 a b φ2)
then have F_is: "F = Until_mltl (convert_nnf φ1) a b (convert_nnf φ2)"
using less by auto
then have G_inset: "G ∈ {(convert_nnf φ1), (convert_nnf φ2)} ∪ subformulas (convert_nnf φ1) ∪
subformulas (convert_nnf φ2)" using less(3) by simp
have depth_phi1: "depth_mltl φ1 < depth_mltl init_F"
using less Until_mltl by simp
have depth_phi2: "depth_mltl φ2 < depth_mltl init_F"
using less Until_mltl by simp
then show ?thesis using less.hyps[OF depth_phi1, of "convert_nnf φ1"] using less.hyps[OF depth_phi2, of "convert_nnf φ2"]
G_inset by blast
next
case (Release_mltl φ1 a b φ2)
then have F_is: "F = Release_mltl (convert_nnf φ1) a b (convert_nnf φ2)"
using less by auto
then have G_inset: "G ∈ {(convert_nnf φ1), (convert_nnf φ2)} ∪ subformulas (convert_nnf φ1) ∪
subformulas (convert_nnf φ2)" using less(3) by simp
have depth_phi1: "depth_mltl φ1 < depth_mltl init_F"
using less Release_mltl by simp
have depth_phi2: "depth_mltl φ2 < depth_mltl init_F"
using less Release_mltl by simp
then show ?thesis using less.hyps[OF depth_phi1, of "convert_nnf φ1"] using less.hyps[OF depth_phi2, of "convert_nnf φ2"]
G_inset by blast
qed
qed
subsection ‹Computation Length and Properties›
fun complen_mltl:: "'a mltl ⇒ nat"
where "complen_mltl False⇩m = 1"
| "complen_mltl True⇩m = 1"
| "complen_mltl Prop⇩m (p) = 1"
| "complen_mltl (Not⇩m φ) = complen_mltl φ"
| "complen_mltl (φ And⇩m ψ) = max (complen_mltl φ) (complen_mltl ψ)"
| "complen_mltl (φ Or⇩m ψ) = max (complen_mltl φ) (complen_mltl ψ)"
| "complen_mltl (G⇩m [a,b] φ) = b + (complen_mltl φ)"
| "complen_mltl (F⇩m [a,b] φ) = b + (complen_mltl φ)"
| "complen_mltl (φ R⇩m [a,b] ψ) = b + (max ((complen_mltl φ)-1) (complen_mltl ψ))"
| "complen_mltl (φ U⇩m [a,b] ψ) = b + (max ((complen_mltl φ)-1) (complen_mltl ψ))"
lemma complen_geq_one: "complen_mltl F ≥ 1"
apply (induct F) apply simp_all .
subsubsection ‹Capture (not (a <= b)) in an MLTL formula›
fun make_empty_trace:: "nat ⇒ 'a set list"
where "make_empty_trace 0 = []"
| "make_empty_trace n = [{}]@ make_empty_trace (n-1)"
lemma length_make_empty_trace:
shows "length (make_empty_trace n) = n"
proof (induct n)
case 0
then show ?case by auto
next
case (Suc n)
then show ?case by auto
qed
lemma semantics_of_not_a_lteq_b:
shows "(make_empty_trace (a+1)) ⊨⇩m (Global_mltl a b True⇩m) = (a ≤ b)"
using length_make_empty_trace
by simp
lemma semantics_of_not_a_lteq_b2:
shows "(make_empty_trace (a+1)) ⊨⇩m (Not_mltl (Global_mltl a b True⇩m)) = (¬ (a ≤ b))"
using semantics_of_not_a_lteq_b
by simp
subsection ‹Custom Induction Rules›
text ‹ In some cases, it is sufficient to consider
just a subset of MLTL operators when proving a property.
We facilitate this with the following custom induction
rules. ›
text ‹ In order to use the MLTL-induct rule,
one must establish IntervalsWellDef, which
states that the input formula is well-formed,
and also prove PProp, which states that the
property being established is not dependent on
the syntax of the input formula but only on its
semantics. ›
lemma MLTL_induct[case_names IntervalsWellDef PProp True False Prop Not And Until]:
assumes IntervalsWellDef: "intervals_welldef F"
and PProp: "(⋀ F G. ((∀π. semantics_mltl π F = semantics_mltl π G) ⟶ P F = P G))"
and True: "P True⇩m"
and False: "P False⇩m"
and Prop: "⋀ p. P Prop⇩m (p)"
and Not: "⋀ F G. ⟦F = Not⇩m G; P G⟧ ⟹ P F"
and And: "⋀F F1 F2. ⟦F = F1 And⇩m F2;
P F1; P F2⟧ ⟹ P F"
and Until:"⋀F F1 F2 a b. ⟦F = F1 U⇩m [a,b] F2;
P F1; P F2⟧ ⟹ P F"
shows "P F" using IntervalsWellDef
proof (induction F)
case True_mltl
then show ?case using True by simp
next
case False_mltl
then show ?case using False by simp
next
case (Prop_mltl x)
then show ?case using Prop by simp
next
case (Not_mltl F1)
then show ?case using Not by auto
next
case (And_mltl F1 F2)
then show ?case using And by auto
next
case (Or_mltl F1 F2)
have "⋀ π. semantics_mltl π (Or_mltl (Not_mltl (Not_mltl F1)) (Not_mltl (Not_mltl F2))) =
semantics_mltl π (Or_mltl F1 F2)"
using not_not_equiv
by auto
then have P1: "P (Or_mltl F1 F2) = P (Or_mltl (Not_mltl (Not_mltl F1)) (Not_mltl (Not_mltl F2)))"
using PProp by blast
have "⋀ π. semantics_mltl π (Not_mltl (And_mltl (Not_mltl F1) (Not_mltl F2))) =
semantics_mltl π (Or_mltl (Not_mltl (Not_mltl F1)) (Not_mltl (Not_mltl F2)))"
using demorgan_and_or[of "(Not_mltl F1)" "(Not_mltl F2)"]
unfolding semantic_equiv_def by simp
then have P2: "P (Not_mltl (And_mltl (Not_mltl F1) (Not_mltl F2))) = P (Or_mltl (Not_mltl (Not_mltl F1)) (Not_mltl (Not_mltl F2)))"
using PProp by blast
show ?case using P1 P2
using And Not PProp
using Or_mltl.IH(1) Or_mltl.IH(2) Or_mltl.prems by force
next
case (Future_mltl a b F)
then show ?case
using future_as_until PProp IntervalsWellDef Until True
unfolding semantic_equiv_def
by (metis True Until intervals_welldef.simps(7))
next
case (Global_mltl a b F)
then show ?case using globally_future_dual Not PProp True Until future_as_until
unfolding semantic_equiv_def
by (metis intervals_welldef.simps(8))
next
case (Until_mltl F1 a b F2)
then show ?case using Until using intervals_welldef.simps(9)[of F1 a b F2]
by blast
next
case (Release_mltl F1 a b F2)
have a_lt_b: "a ≤ b" using Release_mltl(3) intervals_welldef.simps(10)[of F1 a b F2]
by auto
have PF: "P F1 ∧ P F2"
using Release_mltl using intervals_welldef.simps(10)[of F1 a b F2]
by blast
have "P (Release_mltl F1 a b F2) ⟷ P (Not_mltl (Until_mltl (Not_mltl F1) a b (Not_mltl F2)))"
using release_until_dual[OF a_lt_b, of F1 F2] PProp
unfolding semantic_equiv_def by metis
then show ?case using Not
using PF Until by force
qed
text ‹ In order to use the nnf-induct rule,
one must establish that the input formula (i.e.
the formula being inducted on) is in NNF format. ›
lemma nnf_induct[case_names nnf True False Prop And Or Final Global Until Release NotProp]:
assumes nnf: "∃init_F. F = convert_nnf init_F"
and True: "P True⇩m"
and False: "P False⇩m"
and Prop: "⋀ p. P Prop⇩m (p)"
and And: "⋀F F1 F2. ⟦F = F1 And⇩m F2;
P F1; P F2⟧ ⟹ P F"
and Or: "⋀F F1 F2. ⟦F = F1 Or⇩m F2;
P F1; P F2⟧ ⟹ P F"
and Final: "⋀F F1 a b. ⟦F = F⇩m [a,b] F1;
P F1⟧ ⟹ P F"
and Global: "⋀F F1 a b. ⟦F = G⇩m [a,b] F1;
P F1⟧ ⟹ P F"
and Until: "⋀F F1 F2 a b. ⟦F = F1 U⇩m [a,b] F2;
P F1; P F2⟧ ⟹ P F"
and Release: "⋀F F1 F2 a b. ⟦F = F1 R⇩m [a,b] F2;
P F1; P F2⟧ ⟹ P F"
and Not_Prop: "⋀ F p. F = Not⇩m Prop⇩m (p) ⟹ P F"
shows "P F" using nnf proof (induct F)
case True_mltl
then show ?case using True by auto
next
case False_mltl
then show ?case using False by auto
next
case (Prop_mltl x)
then show ?case using Prop by auto
next
case (Not_mltl F)
then show ?case using convert_nnf_form_Not_Implies_Prop Not_Prop by blast
next
case (And_mltl F1 F2)
then obtain init_F where init_F: "And_mltl F1 F2 = convert_nnf init_F"
by auto
then have "(∃init_F1. F1 = convert_nnf init_F1) ∧ (∃init_F2. F2 = convert_nnf init_F2)"
using nnf_subformulas[OF init_F] subformulas.simps(5) by blast
then show ?case using And_mltl And by auto
next
case (Or_mltl F1 F2)
then obtain init_F where init_F: "Or_mltl F1 F2 = convert_nnf init_F"
by auto
then have "(∃init_F1. F1 = convert_nnf init_F1) ∧ (∃init_F2. F2 = convert_nnf init_F2)"
using nnf_subformulas[OF init_F] subformulas.simps(6) by blast
then show ?case using Or_mltl Or by auto
next
case (Future_mltl a b F)
then obtain init_F where init_F: "Future_mltl a b F = convert_nnf init_F"
by auto
then have "(∃init_F1. F = convert_nnf init_F1)"
using nnf_subformulas[OF init_F] subformulas.simps(8) by blast
then show ?case using Future_mltl Final by auto
next
case (Global_mltl a b F)
then obtain init_F where init_F: "Global_mltl a b F = convert_nnf init_F"
by auto
then have "(∃init_F1. F = convert_nnf init_F1)"
using nnf_subformulas[OF init_F] subformulas.simps(7) by blast
then show ?case using Global_mltl Global by auto
next
case (Until_mltl F1 a b F2)
then obtain init_F where init_F: "Until_mltl F1 a b F2 = convert_nnf init_F"
by auto
then have "(∃init_F1. F1 = convert_nnf init_F1) ∧ (∃init_F2. F2 = convert_nnf init_F2)"
using nnf_subformulas[OF init_F] subformulas.simps(9) by blast
then show ?case using Until_mltl Until by auto
next
case (Release_mltl F1 a b F2)
then obtain init_F where init_F: "Release_mltl F1 a b F2 = convert_nnf init_F"
by auto
then have "(∃init_F1. F1 = convert_nnf init_F1) ∧ (∃init_F2. F2 = convert_nnf init_F2)"
using nnf_subformulas[OF init_F] subformulas.simps(10) by blast
then show ?case using Release_mltl Release by auto
qed
end