Theory MLTL_Formula_Progression
section ‹ MLTL formula progresion ›
theory MLTL_Formula_Progression
imports Mission_Time_LTL.MLTL_Properties
begin
subsection ‹Algorithm›
fun weight_operators:: "'a mltl ⇒ nat" where
"weight_operators True⇩m = 1"
| "weight_operators False⇩m = 1"
| "weight_operators (Prop⇩m (p)) = 1"
| "weight_operators (F1 And⇩m F2) = weight_operators F1 + weight_operators F2 + 1"
| "weight_operators (F1 Or⇩m F2) = weight_operators F1 + weight_operators F2 + 1"
| "weight_operators (Not⇩m F) = 1 + weight_operators F "
| "weight_operators (F1 U⇩m [a,b] F2) = weight_operators F1 + weight_operators F2 + 1 + a+ b"
| "weight_operators (F1 R⇩m [a,b] F2) = 10 + weight_operators F1 + weight_operators F2 + 1+ a+ b"
| "weight_operators (G⇩m [a,b] F) = 10 + weight_operators F+ a+ b"
| "weight_operators (F⇩m [a,b] F) = 1 + weight_operators F+ a+ b"
function formula_progression_len1:: "'a mltl ⇒ 'a set ⇒ 'a mltl" where
"formula_progression_len1 True⇩m tr_entry = True⇩m"
| "formula_progression_len1 False⇩m tr_entry = False⇩m"
| "formula_progression_len1 (Prop⇩m (p)) tr_entry = (if p ∈ tr_entry then True⇩m else False⇩m)"
| "formula_progression_len1 (Not⇩m F) tr_entry = Not⇩m (formula_progression_len1 F tr_entry)"
| "formula_progression_len1 (F1 And⇩m F2) tr_entry = (formula_progression_len1 F1 tr_entry) And⇩m (formula_progression_len1 F2 tr_entry) "
| "formula_progression_len1 (F1 Or⇩m F2) tr_entry = (formula_progression_len1 F1 tr_entry) Or⇩m (formula_progression_len1 F2 tr_entry) "
| "formula_progression_len1 (F1 U⇩m [a,b] F2) tr_entry =
(if (0<a ∧ a≤b) then (F1 U⇩m [(a-1), (b-1)] F2)
else (if (0=a ∧ a<b) then ((formula_progression_len1 F2 tr_entry) Or⇩m ((formula_progression_len1 F1 tr_entry) And⇩m (F1 U⇩m [0, (b-1)] F2)))
else (formula_progression_len1 F2 tr_entry)))"
| "formula_progression_len1 (F1 R⇩m [a,b] F2) tr_entry = Not⇩m (formula_progression_len1 ((Not⇩m F1) U⇩m [a,b] (Not⇩m F2)) tr_entry)"
| "formula_progression_len1 (G⇩m [a,b] F) tr_entry = Not⇩m (formula_progression_len1 (F⇩m [a,b] (Not⇩m F)) tr_entry)"
| "formula_progression_len1 (F⇩m [a,b] F) tr_entry =
(if 0< a ∧ a≤ b then (F⇩m [(a-1), (b-1)] F)
else if (0 = a ∧ a < b) then ((formula_progression_len1 F tr_entry) Or⇩m (F⇩m [0, (b-1)] F))
else (formula_progression_len1 F tr_entry))"
by pat_completeness auto
termination by (relation "measure (λ(F,tr_entry). (weight_operators F))") auto
text ‹ Note that formula progression needs to be defined when the
length of the trace is 0. In this case, we define it to just
return the original formula. ›
fun formula_progression:: "'a mltl ⇒ 'a set list ⇒ 'a mltl"
where "formula_progression F tr =
(if length tr = 0 then F
else (if length tr = 1 then (formula_progression_len1 F (tr!0))
else (formula_progression (formula_progression_len1 F (tr ! 0)) (drop 1 tr))))"
value "take 2 ([0::nat, 1, 2, 3]::nat list)"
value "drop 2 ([0::nat, 1, 2, 3]::nat list)"
lemma formula_progression_alt:
"formula_progression F xs = fold (λx F. formula_progression_len1 F x) xs F"
apply (induct xs arbitrary: F)
apply (subst formula_progression.simps; simp_all)
by (smt (verit, best) Cons_nth_drop_Suc One_nat_def diff_Suc_Suc drop0 fold_simps(2) formula_progression.elims length_0_conv length_drop length_greater_0_conv list.discI list.simps(1) zero_diff)
subsection ‹Proofs›
subsubsection ‹Empty Trace Semantics of MLTL›
lemma semantics_global:
shows "[] ⊨⇩m (G⇩m [0,1] φ)"
using semantics_mltl.simps(8)
by blast
lemma semantics_future:
shows "[] ⊨⇩m (Not⇩m (F⇩m [0,1] (Not⇩m φ)))"
using semantics_mltl.simps(7)
semantics_mltl.simps(4) by simp
subsubsection ‹Well-definedness Properties›
lemma formula_progression_well_definedness_preserved_len1:
assumes "intervals_welldef φ"
shows "intervals_welldef (formula_progression_len1 φ π)"
using assms apply (induct φ) using diff_le_mono by simp_all
lemma formula_progression_well_definedness_preserved:
assumes "intervals_welldef φ"
shows "intervals_welldef (formula_progression φ π)"
using assms apply (induct π arbitrary: φ) apply simp
unfolding formula_progression_alt
by (simp add: formula_progression_well_definedness_preserved_len1)
subsubsection ‹Theorem 1›
text ‹ Helper lemma for Theorem 1 ›
lemma formula_progression_identity:
fixes φ::"'a mltl"
fixes k::"nat"
assumes "k < length π"
shows "formula_progression (formula_progression φ (take k π)) [π ! k]
= formula_progression φ (take (k+1) π)"
using assms
proof (induct k arbitrary: π φ)
case 0
then have len_take1: "length (take 1 π) = 1"
by (simp add: Suc_leI)
then have same_fp: "formula_progression φ [π ! 0] = formula_progression φ (take 1 π)"
by auto
have "take 0 π = []"
by auto
then have "formula_progression φ (take 0 π) = φ"
by auto
then show ?case
using same_fp by auto
next
case (Suc k)
{assume *: "Suc k = 1"
then have len_pi: "length π ≥ 2"
using Suc(2) by auto
then have take2: "take 2 π = [π ! 0, π ! 1]"
by (smt (verit) "*" Cons_nth_drop_Suc One_nat_def Suc.prems Suc_1 dual_order.strict_trans id_take_nth_drop less_numeral_extra(1) self_append_conv2 take0 take_Suc_Cons)
have take1: "take 1 π = [π ! 0]"
using len_pi
by (metis "*" Cons_eq_append_conv One_nat_def Suc.prems dual_order.strict_trans less_numeral_extra(1) take0 take_Suc_conv_app_nth)
have "formula_progression (formula_progression φ [π ! 0])
[π ! 1] =
formula_progression φ [π ! 0, π ! 1]"
by fastforce
then have ?case
using * take1 take2
using Suc_1 plus_1_eq_Suc by presburger
} moreover {assume *: "Suc k > 1"
have "formula_progression φ (take (Suc k + 1) π) =
formula_progression (formula_progression φ [π ! 0]) (drop 1 (take (Suc k + 1) π))"
using Suc by simp
let ?ψ = "formula_progression φ [π ! 0]"
let ?ξ = "drop 1 π"
have "drop 1 (take (Suc k + 1) π) = take (k+1) ?ξ"
by (simp add: drop_take)
have ih_prem: "k < length (take (k+1) ?ξ)"
using Suc(2) by simp
have "take k (take (k + 1) (drop 1 π)) = take k (drop 1 π)"
by simp
then have "formula_progression (formula_progression φ [π ! 0])
(take k (take (k + 1) (drop 1 π))) = formula_progression φ (take (k+1) π)"
using Suc(2) *
by (smt (verit) Nat.add_diff_assoc Nat.diff_diff_right add_diff_cancel_left' diff_add_zero drop_take dual_order.strict_trans formula_progression.elims leI le_numeral_extra(4) length_Cons length_take less_2_cases_iff list.size(3) min.absorb4 not_less_iff_gr_or_eq nth_Cons_0 nth_take plus_1_eq_Suc zero_less_one zero_neq_one)
then have ?case
using Suc(1)[OF ih_prem, of ?ψ]
by (smt (verit) "*" One_nat_def Suc.hyps Suc.prems Suc_eq_plus1 ‹drop 1 (take (Suc k + 1) π) = take (k + 1) (drop 1 π)› ‹formula_progression φ (take (Suc k + 1) π) = formula_progression (formula_progression φ [π ! 0]) (drop 1 (take (Suc k + 1) π))› ‹take k (take (k + 1) (drop 1 π)) = take k (drop 1 π)› drop_all dual_order.strict_trans length_drop length_greater_0_conv less_diff_conv nle_le nth_drop plus_1_eq_Suc)
}
ultimately show ?case using Suc(2)
by auto
qed
text ‹ Theorem 1 ›
theorem formula_progression_decomposition:
fixes φ::"'a mltl"
assumes "k ≥ 1"
assumes "k ≤ length π"
shows "formula_progression (formula_progression φ (take k π)) (drop k π)
= formula_progression φ π"
using assms
proof (induct k)
case 0
then show ?case by simp
next
case (Suc k)
{assume *: "Suc k = 1"
{assume **: "length π = 1"
have h1: "formula_progression φ π =
formula_progression_len1 φ (π ! 0)"
using * **
by (metis formula_progression.simps zero_neq_one)
have h2a:"formula_progression (formula_progression φ (take (Suc k) π))
(drop (Suc k) π) = formula_progression φ (take (Suc k) π)"
using * **
by simp
have h2b: "formula_progression φ (take (Suc k) π) = formula_progression_len1 φ (π!0)"
using * **
using h1 by auto
have ?case using h1 h2a h2b
by argo
} moreover {assume ** : "length π > 1"
then have h1: "formula_progression φ π = formula_progression (formula_progression_len1 φ (π ! 0))
(drop 1 π)"
using formula_progression.simps[of φ π]
by auto
then have h2: "formula_progression (formula_progression φ (take (Suc k) π))
(drop (Suc k) π) = formula_progression (formula_progression φ ([π!0]))
(drop 1 π)"
using *
by (metis "**" One_nat_def Suc_lessD append_Nil take_0 take_Suc_conv_app_nth)
have "(formula_progression φ [π ! 0]) = formula_progression_len1 φ (π ! 0)"
using formula_progression.simps by simp
then have ?case
using * h1 h2 by simp
}
ultimately have ?case
using Suc.prems(2) by linarith
} moreover {assume *: "Suc k > 1"
then have simplify1: "formula_progression (formula_progression φ (take k π)) (drop k π)
= formula_progression
(formula_progression_len1
(formula_progression φ (take k π)) (drop k π ! 0))
(drop 1 (drop k π))"
using formula_progression.simps[of "formula_progression φ (take k π)" "(drop k π)"]
Suc(3)
by (metis cancel_comm_monoid_add_class.diff_cancel diff_is_0_eq formula_progression.elims length_drop not_less_eq_eq)
have simplify2: "drop k π ! 0= π!k ∧ drop 1 (drop k π) = drop (k+1) π"
using * Suc(3)
by (metis Cons_nth_drop_Suc Suc_eq_plus1 Suc_le_lessD drop_drop nth_Cons_0 plus_1_eq_Suc)
then have simplify3: "formula_progression (formula_progression φ (take k π)) (drop k π)
= formula_progression
(formula_progression_len1
(formula_progression φ (take k π)) (π!k))
(drop (k+1) π)"
using simplify1 by presburger
have "(formula_progression (formula_progression φ (take k π)) ([π ! k])) =
formula_progression_len1 (formula_progression φ (take k π)) (π!k)"
by simp
then have equality1: "formula_progression (formula_progression φ (take k π)) (drop k π)
= formula_progression (formula_progression (formula_progression φ (take k π)) ([π ! k])) (drop (k+1) π)"
using simplify3 by presburger
have equality2: "formula_progression (formula_progression φ (take k π)) ([π ! k]) = formula_progression φ (take (k+1) π)"
using * Suc(3) formula_progression_identity Suc_le_lessD
by blast
then have ?case
by (metis "*" Suc.hyps Suc.prems(2) Suc_eq_plus1 Suc_leD ‹formula_progression (formula_progression φ (take k π)) [π ! k] = formula_progression_len1 (formula_progression φ (take k π)) (π ! k)› less_Suc_eq_le simplify3)
}
ultimately show ?case
by linarith
qed
subsubsection ‹Theorem 2›
text ‹ Base case for Theorem 2 ›
lemma satisfiability_preservation_len1:
fixes φ::"'a mltl"
assumes "1 < length π"
assumes "intervals_welldef φ"
shows "semantics_mltl (drop 1 π) (formula_progression_len1 φ (π ! 0))
⟷ semantics_mltl π φ"
using assms
proof (induction φ)
case True_mltl
then show ?case by auto
next
case False_mltl
then show ?case by auto
next
case (Prop_mltl p)
then show ?case using formula_progression_len1.simps(3)[of p "π ! 0"]
using Prop_mltl by force
next
case (Not_mltl F)
then show ?case by simp
next
case (And_mltl F1 F2)
then show ?case by simp
next
case (Or_mltl F1 F2)
then show ?case by simp
next
case (Future_mltl a b F)
{assume * :"0 < a ∧ a ≤ b"
have equiv: "((a - 1 ≤ i ∧ i ≤ b - 1) ∧ semantics_mltl (drop i (drop 1 π)) F) ⟷
((a ≤ (i+1) ∧ (i+1) ≤ b) ∧ semantics_mltl (drop (i+1) π) F)"
for i
using "*" Nat.le_diff_conv2 le_diff_conv by auto
have d1: "(∃i. (a - 1 ≤ i ∧ i ≤ b - 1) ∧
semantics_mltl (drop i (drop 1 π)) F) ⟶
(∃i. (a ≤ i ∧ i ≤ b) ∧ semantics_mltl (drop i π) F)"
using equiv by auto
have d2: "(∃i. (a ≤ i ∧ i ≤ b) ∧ semantics_mltl (drop i π) F) ⟶
(∃i. (a - 1 ≤ i ∧ i ≤ b - 1) ∧
semantics_mltl (drop i (drop 1 π)) F)"
using equiv
by (metis "*" Suc_diff_Suc Suc_eq_plus1 diff_zero linorder_not_less not_gr_zero)
then have "(∃i. (a - 1 ≤ i ∧ i ≤ b - 1) ∧
semantics_mltl (drop i (drop 1 π)) F) ⟷
(∃i. (a ≤ i ∧ i ≤ b) ∧ semantics_mltl (drop i π) F)"
using d1 d2 by auto
then have "semantics_mltl (drop 1 π) (Future_mltl (a - 1) (b - 1) F) =
semantics_mltl π (Future_mltl a b F)"
using semantics_mltl.simps(7)[of "(drop 1 π)" "a - 1" "b - 1" F]
semantics_mltl.simps(7)[of "π" "a" "b" F] *
using dual_order.trans by auto
then have ?case
using formula_progression_len1.simps(10)[of a b F "π ! 0"]
using "*"
by presburger
}
moreover {assume *: "0 = a ∧ a < b"
have fp_is: "formula_progression_len1 (Future_mltl a b F) (π ! 0) =
Or_mltl (formula_progression_len1 F (π ! 0)) (Future_mltl 0 (b - 1) F)"
using * by auto
have length_gt:"length π > 0"
using Future_mltl by auto
have rhs: "semantics_mltl π (Future_mltl a b F) = (a < length π ∧ (∃i. (a ≤ i ∧ i ≤ b) ∧ semantics_mltl (drop i π) F))"
using semantics_mltl.simps(7)[of π a b F] * by auto
have "semantics_mltl (drop 1 π) (Or_mltl (formula_progression_len1 F (π ! 0)) (Future_mltl 0 (b - 1) F))
= (semantics_mltl (drop 1 π) (formula_progression_len1 F (π ! 0))) ∨ (semantics_mltl (drop 1 π) (Future_mltl 0 (b - 1) F))"
by auto
then have lhs:"semantics_mltl (drop 1 π) (formula_progression_len1 (Future_mltl a b F) (π ! 0)) =
(semantics_mltl (drop 1 π) (formula_progression_len1 F (π ! 0))) ∨ (semantics_mltl (drop 1 π) (Future_mltl 0 (b - 1) F))"
using fp_is
by simp
have b_prop: "b-1 ≥ 0" using * by auto
have "((∃i. (0 ≤ i ∧ i ≤ b) ∧ semantics_mltl (drop i π) F)) =
(semantics_mltl π F ∨
(0 < length (drop 1 π) ∧ (∃i. (0 ≤ i ∧ i ≤ b - 1) ∧ semantics_mltl (drop (i+1) π) F)))"
proof -
{assume **: "length π = 1"
then have ?thesis using * Future_mltl by auto
} moreover {assume **: "length π > 1"
have h1: "(∃i. (0 ≤ i ∧ i ≤ b) ∧ semantics_mltl (drop i π) F) ⟶
(semantics_mltl π F ∨ (∃i. (0 ≤ i ∧ i ≤ b - 1) ∧ semantics_mltl (drop (i + 1) π) F))"
by (metis Suc_eq_plus1 Suc_pred' bot_nat_0.extremum diff_le_mono drop_0 le_imp_less_Suc less_one linorder_le_less_linear)
have h2: "(semantics_mltl π F ∨ (∃i. (0 ≤ i ∧ i ≤ b - 1) ∧ semantics_mltl (drop (i + 1) π) F)) ⟶
(∃i. (0 ≤ i ∧ i ≤ b) ∧ semantics_mltl (drop i π) F)"
by (metis "*" Nat.le_diff_conv2 drop0 gr_implies_not0 less_one linorder_le_less_linear zero_le)
have "(∃i. (0 ≤ i ∧ i ≤ b) ∧ semantics_mltl (drop i π) F) =
(semantics_mltl π F ∨ (∃i. (0 ≤ i ∧ i ≤ b - 1) ∧ semantics_mltl (drop (i + 1) π) F))"
using h1 h2 by auto
then have ?thesis
using **
by simp
}
ultimately show ?thesis using Future_mltl(2)
by fastforce
qed
then have "(a < length π ∧ (∃i. (a ≤ i ∧ i ≤ b) ∧ semantics_mltl (drop i π) F)) =
(semantics_mltl π F ∨ (0 ≤ b - 1 ∧
0 < length (drop 1 π) ∧ (∃i. (0 ≤ i ∧ i ≤ b - 1) ∧ semantics_mltl (drop i (drop 1 π)) F)))"
using length_gt * by auto
then have "(a < length π ∧ (∃i. (a ≤ i ∧ i ≤ b) ∧ semantics_mltl (drop i π) F)) =
(semantics_mltl π F ∨ (semantics_mltl (drop 1 π) (Future_mltl 0 (b - 1) F)))"
using semantics_mltl.simps(7)[of "(drop 1 π)" 0 "b-1" F]
by simp
then have "(a < length π ∧ (∃i. (a ≤ i ∧ i ≤ b) ∧ semantics_mltl (drop i π) F)) =
(semantics_mltl (drop 1 π) (formula_progression_len1 F (π ! 0))) ∨ (semantics_mltl (drop 1 π) (Future_mltl 0 (b - 1) F))"
using Future_mltl
by (metis intervals_welldef.simps(7))
then have ?case
using lhs rhs fp_is * Future_mltl
by fastforce
} moreover {assume * :"¬(0 = a ∧ a < b) ∧ ¬ (0 < a ∧ a ≤ b)"
then have a_eq_b: "a = 0 ∧ b = 0"
using Future_mltl(3) using intervals_welldef.simps(7)[of a b F]
by auto
then have "formula_progression_len1 (Future_mltl a b F) (π ! 0) = formula_progression_len1 F (π ! 0)"
by auto
then have h1: "semantics_mltl (drop 1 π) (formula_progression_len1 (Future_mltl a b F) (π ! 0)) = semantics_mltl π F"
using Future_mltl
by simp
have "semantics_mltl π F = semantics_mltl π (Future_mltl 0 0 F)"
using semantics_mltl.simps(7)[of "π" 0 0 F] *
Future_mltl(2)
by force
then have ?case
using h1 a_eq_b by blast
}
ultimately show ?case
by blast
next
case (Global_mltl a b F)
have " semantics_mltl (drop 1 π) (formula_progression_len1 (Global_mltl a b F) (π ! 0)) =
(¬ (semantics_mltl (drop 1 π) (formula_progression_len1 (Future_mltl a b (Not_mltl F)) (π ! 0))))"
unfolding formula_progression_len1.simps by auto
have "((formula_progression_len1 (Future_mltl a b (Not_mltl F)) (π ! 0))) =
(if 0 < a ∧ a ≤ b then Future_mltl (a - 1) (b - 1) (Not_mltl F)
else if 0 = a ∧ a < b
then Or_mltl (formula_progression_len1 (Not_mltl F) (π ! 0))
(Future_mltl 0 (b - 1) (Not_mltl F))
else formula_progression_len1 (Not_mltl F) (π ! 0))"
using formula_progression_len1.simps(10)
by simp
{assume *: "0 < a ∧ a ≤ b"
have d1: "(∀i. ((a - 1 ≤ i ∧ i ≤ b - 1) ⟶ semantics_mltl (drop (i+1) π) F)) ⟹ (⋀i. a ≤ i ∧ i ≤ b ⟹ semantics_mltl (drop i π) F)"
proof -
fix i
assume all_prop: "(∀i. ((a - 1 ≤ i ∧ i ≤ b - 1) ⟶ semantics_mltl (drop (i+1) π) F))"
assume " a ≤ i ∧ i ≤ b"
then have "a-1 ≤ i-1 ∧ i - 1 ≤ b - 1"
by auto
then have "semantics_mltl (drop ((i-1)+1) π) F"
using all_prop by simp
then show " semantics_mltl (drop i π) F"
using assms *
by (metis One_nat_def Suc_leI ‹a ≤ i ∧ i ≤ b› le_add_diff_inverse2 order_less_le_trans)
qed
have d2: "(∀i. a ≤ i ∧ i ≤ b ⟶ semantics_mltl (drop i π) F) ⟹ (⋀i. ((a - 1 ≤ i ∧ i ≤ b - 1) ⟹ semantics_mltl (drop (i+1) π) F))"
proof -
fix i
assume all_prop: "(∀i. a ≤ i ∧ i ≤ b ⟶ semantics_mltl (drop i π) F)"
assume " a-1 ≤ i ∧ i ≤ b-1"
then have "a ≤ i+1 ∧ i+1 ≤ b"
using * by auto
then show "semantics_mltl (drop (i+1) π) F"
using assms * all_prop by blast
qed
have all_conn: "(∀i. (a - 1 ≤ i ∧ i ≤ b - 1) ⟶ semantics_mltl (drop (i+1) π) F) = (∀i. a ≤ i ∧ i ≤ b ⟶ semantics_mltl (drop i π) F)"
using d1 d2 by blast
have "(¬ semantics_mltl (drop 1 π) ( Future_mltl (a - 1) (b - 1) (Not_mltl F))) = (¬ (a - 1 < length (drop 1 π) ∧
(∃i. (a - 1 ≤ i ∧ i ≤ b - 1) ∧ ¬ semantics_mltl (drop i (drop 1 π)) F)))"
using * unfolding semantics_mltl.simps by auto
then have "(¬ semantics_mltl (drop 1 π) ( Future_mltl (a - 1) (b - 1) (Not_mltl F))) = ((a - 1 ≥ length (drop 1 π) ∨
¬(∃i. (a - 1 ≤ i ∧ i ≤ b - 1) ∧ ¬ semantics_mltl (drop i (drop 1 π)) F)))"
by auto
then have "(¬ semantics_mltl (drop 1 π) ( Future_mltl (a - 1) (b - 1) (Not_mltl F))) = (a ≥ length π ∨
(∀i. ((a - 1 ≤ i ∧ i ≤ b - 1) ⟶ semantics_mltl (drop i (drop 1 π)) F)))"
by (metis "*" One_nat_def Suc_le_mono Suc_pred assms(1) length_0_conv length_drop length_greater_0_conv not_one_less_zero)
then have "(¬ semantics_mltl (drop 1 π) ( Future_mltl (a - 1) (b - 1) (Not_mltl F))) =
(length π ≤ a ∨ (∀i. (a ≤ i ∧ i ≤ b ⟶ semantics_mltl (drop i π) F)))"
using all_conn by simp
then have ?case unfolding formula_progression_len1.simps semantics_mltl.simps
using * by auto
} moreover {assume *: " 0 = a ∧ a < b"
have d1: "(∀i. (0 ≤ i ∧ i ≤ b - 1) ⟶ semantics_mltl (drop (i+1) π) F) ⟹ (⋀i. 1 ≤ i ∧ i ≤ b ⟹ semantics_mltl (drop i π) F)"
proof -
assume all_prop: "(∀i. (0 ≤ i ∧ i ≤ b - 1) ⟶ semantics_mltl (drop (i+1) π) F)"
fix i
assume "1 ≤ i ∧ i ≤ b"
then have "(0 ≤ i-1 ∧ i-1 ≤ b - 1)"
by auto
then show "semantics_mltl (drop i π) F"
using all_prop
by (metis ‹1 ≤ i ∧ i ≤ b› le_add_diff_inverse2)
qed
have d2: "(∀i. 1 ≤ i ∧ i ≤ b ⟶ semantics_mltl (drop i π) F) ⟹ (⋀i. (0 ≤ i ∧ i ≤ b - 1) ⟹ semantics_mltl (drop (i+1) π) F)"
proof -
assume all_prop: "(∀i. 1 ≤ i ∧ i ≤ b ⟶ semantics_mltl (drop i π) F)"
fix i
assume "(0 ≤ i ∧ i ≤ b - 1)"
then have "1 ≤ i+1 ∧ i+1 ≤ b"
using * by auto
then show "semantics_mltl (drop (i+1) π) F"
using all_prop by blast
qed
have "¬(∃i. (0 ≤ i ∧ i ≤ b - 1) ∧ ¬ semantics_mltl (drop (i+1) π) F)
= (∀i. (0 ≤ i ∧ i ≤ b - 1) ⟶ semantics_mltl (drop (i+1) π) F)"
by blast
then have exist_rel: "¬(∃i. (0 ≤ i ∧ i ≤ b - 1) ∧ ¬ semantics_mltl (drop (i+1) π) F)
= (∀i. 1 ≤ i ∧ i ≤ b ⟶ semantics_mltl (drop i π) F)"
using d1 d2 by metis
have eq_2: "semantics_mltl π F = semantics_mltl (drop 0 π) F"
by auto
then have "(semantics_mltl π F ∧
¬(∃i. (0 ≤ i ∧ i ≤ b - 1) ∧ ¬ semantics_mltl (drop (i+1) π) F)) =
(∀i. 0 ≤ i ∧ i ≤ b ⟶ semantics_mltl (drop i π) F)"
using exist_rel eq_2
by (metis One_nat_def Suc_leI bot_nat_0.extremum le_eq_less_or_eq)
then have " (semantics_mltl (drop 1 π) (formula_progression_len1 F (π ! 0)) ∧
¬(∃i. (0 ≤ i ∧ i ≤ b - 1) ∧ ¬ semantics_mltl (drop i (drop 1 π)) F)) =
(∀i. 0 ≤ i ∧ i ≤ b ⟶ semantics_mltl (drop i π) F)"
using Global_mltl by auto
then have " (¬ (¬ semantics_mltl (drop 1 π) (formula_progression_len1 F (π ! 0)) ∨
(∃i. (0 ≤ i ∧ i ≤ b - 1) ∧ ¬ semantics_mltl (drop i (drop 1 π)) F))) =
(∀i. a ≤ i ∧ i ≤ b ⟶ semantics_mltl (drop i π) F)"
using *
by auto
then have "(¬ semantics_mltl (drop 1 π)
(Or_mltl (Not_mltl (formula_progression_len1 F (π ! 0)))
(Future_mltl 0 (b - 1) (Not_mltl F)))) =
(length π ≤ a ∨ (∀i. a ≤ i ∧ i ≤ b ⟶ semantics_mltl (drop i π) F))"
using * Global_mltl unfolding semantics_mltl.simps by auto
then have ?case using * unfolding formula_progression_len1.simps semantics_mltl.simps
by auto
} moreover {assume *: "¬(0 < a ∧ a ≤ b) ∧ ¬(0 = a ∧ a < b)"
have "a ≤ b"
using Global_mltl(3) unfolding intervals_welldef.simps
by auto
then have **: "0 = a ∧ 0 = b"
using * by auto
have ind_h: "semantics_mltl (drop 1 π) (formula_progression_len1 F (π ! 0)) = semantics_mltl π F"
using Global_mltl by auto
have "semantics_mltl π F =
(length π ≤ 0 ∨ (∀i. 0 ≤ i ∧ i ≤ 0 ⟶ semantics_mltl (drop i π) F))"
using Global_mltl by auto
then have "(¬ semantics_mltl (drop 1 π)
(Not_mltl (formula_progression_len1 F (π ! 0)))) =
(a ≤ b ∧ (length π ≤ a ∨ (∀i. a ≤ i ∧ i ≤ b ⟶ semantics_mltl (drop i π) F)))"
using ind_h ** unfolding semantics_mltl.simps by blast
then have ?case using * unfolding formula_progression_len1.simps semantics_mltl.simps
by force
}
ultimately show ?case by blast
next
case (Until_mltl F1 a b F2)
{assume *: "0 < a ∧ a ≤ b"
have d1: "(∃i. (a ≤ i ∧ i ≤ b) ∧ semantics_mltl (drop i π) F2 ∧ (∀j. a ≤ j ∧ j < i ⟶ semantics_mltl (drop j π) F1))"
if i_ex: "(∃i. (a - 1 ≤ i ∧ i ≤ b - 1) ∧ semantics_mltl (drop (i + 1) π) F2 ∧
(∀j. a - 1 ≤ j ∧ j < i ⟶ semantics_mltl (drop (j + 1) π) F1))"
proof -
obtain i where i_sat: "(a - 1 ≤ i ∧ i ≤ b - 1)"
"semantics_mltl (drop (i + 1) π) F2"
"(⋀j. a - 1 ≤ j ∧ j < i ⟹ semantics_mltl (drop (j + 1) π) F1)"
using i_ex by auto
have h1: "a ≤ i + 1 ∧ i + 1 ≤ b"
using * i_sat by auto
have h2: "semantics_mltl (drop (i+1) π) F2"
using i_sat by blast
have h3: "semantics_mltl (drop j π) F1" if j: "a ≤ j ∧ j < (i+1)" for j
using i_sat(3)[of "j-1"] j
by (metis (no_types, lifting) "*" One_nat_def Suc_eq_plus1 Suc_leI le_add_diff_inverse2 le_imp_less_Suc linorder_not_less order_less_le_trans)
then show ?thesis using h1 h2 h3 by auto
qed
have d2: "(∃i. (a - 1 ≤ i ∧ i ≤ b - 1) ∧ semantics_mltl (drop (i + 1) π) F2 ∧
(∀j. a - 1 ≤ j ∧ j < i ⟶ semantics_mltl (drop (j + 1) π) F1))"
if i_ex: "(∃i. (a ≤ i ∧ i ≤ b) ∧
semantics_mltl (drop i π) F2 ∧ (∀j. a ≤ j ∧ j < i ⟶ semantics_mltl (drop j π) F1))"
proof -
obtain i where i_sat: "(a ≤ i ∧ i ≤ b)"
"semantics_mltl (drop i π) F2"
"(⋀j. a ≤ j ∧ j < i ⟹ semantics_mltl (drop j π) F1)"
using i_ex by auto
then have h1: "a - 1 ≤ i-1 ∧ i-1 ≤ b - 1"
using * i_sat(1) by auto
have h2: "semantics_mltl (drop ((i-1)+1) π) F2"
using i_sat *
by simp
have h3: "semantics_mltl (drop (j+1) π) F1" if j: "a-1 ≤ j ∧ j < i-1" for j
using i_sat(3)[of "j"] j
using i_sat(3) le_diff_conv less_diff_conv by blast
then show ?thesis using h1 h2 h3
by auto
qed
have "(∃i. (a - 1 ≤ i ∧ i ≤ b - 1) ∧ semantics_mltl (drop (i+1) π) F2 ∧
(∀j. a - 1 ≤ j ∧ j < i ⟶ semantics_mltl (drop (j+1) π) F1)) =
(∃i. (a ≤ i ∧ i ≤ b) ∧
semantics_mltl (drop i π) F2 ∧ (∀j. a ≤ j ∧ j < i ⟶ semantics_mltl (drop j π) F1))"
using d1 d2 by blast
then have "(a - 1 < length (drop 1 π) ∧
(∃i. (a - 1 ≤ i ∧ i ≤ b - 1) ∧ semantics_mltl (drop i (drop 1 π)) F2 ∧
(∀j. a - 1 ≤ j ∧ j < i ⟶ semantics_mltl (drop j (drop 1 π)) F1))) =
(a < length π ∧
(∃i. (a ≤ i ∧ i ≤ b) ∧
semantics_mltl (drop i π) F2 ∧ (∀j. a ≤ j ∧ j < i ⟶ semantics_mltl (drop j π) F1)))"
using Until_mltl(3) by auto
then have "semantics_mltl (drop 1 π) (Until_mltl F1 (a - 1) (b - 1) F2) =
semantics_mltl π (Until_mltl F1 a b F2)"
using * unfolding semantics_mltl.simps
by (meson order_trans)
then have ?case unfolding formula_progression_len1.simps
using * by simp
}
moreover {assume *: "0 = a ∧ a < b"
have d1: "(∃i. (0 ≤ i ∧ i ≤ b) ∧
semantics_mltl (drop i π) F2 ∧ (∀j. 0 ≤ j ∧ j < i ⟶ semantics_mltl (drop j π) F1))"
if sem: "(semantics_mltl π F2 ∨ (semantics_mltl π F1 ∧
(∃i. (0 ≤ i ∧ i ≤ b - 1) ∧ semantics_mltl (drop (i+1) π) F2 ∧
(∀j. 0 ≤ j ∧ j < i ⟶ semantics_mltl (drop (j + 1) π) F1))))"
proof -
{assume *: "semantics_mltl π F2"
then have "semantics_mltl (drop 0 π) F2 ∧ (∀j. 0 ≤ j ∧ j < 0 ⟶ semantics_mltl (drop j π) F1)"
by simp
then have ?thesis by blast
} moreover {assume **: "semantics_mltl π F1 ∧ (∃i. (0 ≤ i ∧ i ≤ b - 1) ∧
semantics_mltl (drop (i+1) π) F2 ∧ (∀j. 0 ≤ j ∧ j < i ⟶ semantics_mltl (drop (j + 1) π) F1))"
then obtain i where i_prop: "(0 ≤ i ∧ i ≤ b - 1) ∧ semantics_mltl (drop (i + 1) π) F2 ∧
(∀j. 0 ≤ j ∧ j < i ⟶ semantics_mltl (drop (j + 1) π) F1)"
by auto
have "semantics_mltl (drop 0 π) F1"
using ** by auto
then have "(0 ≤ i ∧ i ≤ b - 1) ∧ semantics_mltl (drop (i + 1) π) F2 ∧
(∀j. 0 ≤ j ∧ j < i+1 ⟶ semantics_mltl (drop j π) F1)"
using i_prop
using less_Suc_eq_0_disj by force
then have "(0 ≤ (i+1) ∧ (i+1) ≤ b) ∧
semantics_mltl (drop (i+1) π) F2 ∧ (∀j. 0 ≤ j ∧ j < (i+1) ⟶ semantics_mltl (drop j π) F1)"
using * by auto
then have ?thesis by blast
}
ultimately show ?thesis using sem by auto
qed
have d2: "(semantics_mltl π F2 ∨
(semantics_mltl π F1 ∧
(∃i. (0 ≤ i ∧ i ≤ b - 1) ∧ semantics_mltl (drop (i+1) π) F2 ∧
(∀j. 0 ≤ j ∧ j < i ⟶ semantics_mltl (drop (j + 1) π) F1))))"
if i_ex: "(∃i. (0 ≤ i ∧ i ≤ b) ∧
semantics_mltl (drop i π) F2 ∧ (∀j. 0 ≤ j ∧ j < i ⟶ semantics_mltl (drop j π) F1))"
proof -
obtain i where i_prop: "(0 ≤ i ∧ i ≤ b) ∧
semantics_mltl (drop i π) F2 ∧ (∀j. 0 ≤ j ∧ j < i ⟶ semantics_mltl (drop j π) F1)"
using i_ex by auto
{assume *: "i = 0"
then have "semantics_mltl (drop 0 π) F2"
using i_prop
by auto
then have "semantics_mltl π F2"
by auto
then have ?thesis by blast
} moreover { assume * : "i > 0"
then have g1: "semantics_mltl π F1"
using i_prop by auto
have i_sem: "(0 ≤ i-1 ∧ i-1 ≤ b) ∧
semantics_mltl (drop ((i-1)+1) π) F2"
using i_prop * by auto
have "⋀j. 0 ≤ j ∧ j < i ⟹ semantics_mltl (drop j π) F1"
using i_prop
by auto
then have "⋀j. 0 ≤ j ∧ j < i-1 ⟹ semantics_mltl (drop (j + 1) π) F1"
using i_prop g1
by (simp add: less_diff_conv)
then have g2: "(0 ≤ i-1 ∧ i-1 ≤ b - 1) ∧
semantics_mltl (drop (i-1 + 1) π) F2 ∧
(∀j. 0 ≤ j ∧ j < i-1 ⟶ semantics_mltl (drop (j + 1) π) F1)"
using i_sem
using diff_le_mono i_prop by presburger
have ?thesis using g1 g2 by auto
}
ultimately show ?thesis
by blast
qed
have "(semantics_mltl π F2 ∨
(semantics_mltl π F1 ∧
(∃i. (0 ≤ i ∧ i ≤ b - 1) ∧ semantics_mltl (drop (i+1) π) F2 ∧
(∀j. 0 ≤ j ∧ j < i ⟶ semantics_mltl (drop (j + 1) π) F1)))) =
((∃i. (0 ≤ i ∧ i ≤ b) ∧
semantics_mltl (drop i π) F2 ∧ (∀j. 0 ≤ j ∧ j < i ⟶ semantics_mltl (drop j π) F1)))"
using d1 d2 by blast
then have "semantics_mltl (drop 1 π)
(Or_mltl (formula_progression_len1 F2 (π ! 0))
(And_mltl (formula_progression_len1 F1 (π ! 0)) (Until_mltl F1 0 (b - 1) F2))
) =
semantics_mltl π (Until_mltl F1 0 b F2)"
unfolding semantics_mltl.simps using * Until_mltl
by auto
then have ?case unfolding formula_progression_len1.simps using *
by auto
}
moreover {assume *: "¬(0 < a ∧ a ≤ b) ∧ ¬(0 = a ∧ a < b)"
then have a_eq_b: "a = 0 ∧ b = 0"
using Until_mltl(4) by auto
then have same_fm1: "(formula_progression_len1 (Until_mltl F1 0 0 F2) (π ! 0)) = formula_progression_len1 F2 (π ! 0)"
by auto
have same_fm2: "semantics_mltl π F2 = semantics_mltl (drop 1 π) (formula_progression_len1 F2 (π ! 0))"
using Until_mltl(2) Until_mltl(3) Until_mltl(4)
by simp
have same_fm3: "semantics_mltl π (Until_mltl F1 0 0 F2) = semantics_mltl π F2"
using semantics_mltl.simps(9)[of π F1 0 0 F2]
using Until_mltl(3) by auto
have "semantics_mltl (drop 1 π) (formula_progression_len1 F2 (π ! 0)) = semantics_mltl π (Until_mltl F1 0 0 F2)"
using same_fm1 same_fm2 same_fm3 by blast
then have "semantics_mltl (drop 1 π) (formula_progression_len1 (Until_mltl F1 0 0 F2) (π ! 0)) =
semantics_mltl π (Until_mltl F1 0 0 F2)"
using same_fm3 by auto
then have ?case using a_eq_b by auto
}
ultimately show ?case by auto
next
case (Release_mltl F1 a b F2)
{assume * :"0< a ∧ a≤ b"
have d1: "(∀i. (a - 1 ≤ i ∧ i ≤ b - 1) ⟶
semantics_mltl (drop i (drop 1 π)) F2 ∨
(∃j. a - 1 ≤ j ∧ j < i ∧ semantics_mltl (drop j (drop 1 π)) F1))"
if all_i: "((∀i. a ≤ i ∧ i ≤ b ⟶ semantics_mltl (drop i π) F2) ∨
(∃j≥a. j ≤ b - 1 ∧ semantics_mltl (drop j π) F1 ∧
(∀k. a ≤ k ∧ k ≤ j ⟶ semantics_mltl (drop k π) F2)))"
proof -
{assume or1: "(∀i. a ≤ i ∧ i ≤ b ⟶ semantics_mltl (drop i π) F2)"
then have "(∀i. (a - 1 ≤ i ∧ i ≤ b - 1) ⟶ semantics_mltl (drop i (drop 1 π)) F2)"
using *
using le_diff_conv by auto
then have ?thesis
by blast
} moreover {assume or2 : "(∃j≥a. j ≤ b - 1 ∧ semantics_mltl (drop j π) F1 ∧
(∀k. a ≤ k ∧ k ≤ j ⟶ semantics_mltl (drop k π) F2))"
then obtain j where j_prop: "j≥a ∧ j ≤ b - 1 ∧
semantics_mltl (drop j π) F1 ∧ (∀k. a ≤ k ∧ k ≤ j ⟶ semantics_mltl (drop k π) F2)"
by blast
then have "semantics_mltl (drop i (drop 1 π)) F2 ∨
(∃j≥a - 1. j < i ∧ semantics_mltl (drop j (drop 1 π)) F1)"
if i_prop: "a - 1 ≤ i ∧ i ≤ b - 1" for i
proof -
{assume j: "j-1 < i"
then have "j-1≥a - 1 ∧ j-1 < i ∧ semantics_mltl (drop (j-1) (drop 1 π)) F1"
using j_prop * by auto
then have ?thesis by blast
} moreover {assume j: "j-1 ≥ i"
then have "j ≥ i+1"
using j_prop * by linarith
then have " semantics_mltl (drop (i+1) π) F2"
using j_prop *
using le_diff_conv that by blast
then have ?thesis by simp
}
ultimately show ?thesis
by force
qed
then have ?thesis by blast
}
ultimately show ?thesis using all_i by blast
qed
have d2: "((∀i. a ≤ i ∧ i ≤ b ⟶ semantics_mltl (drop i π) F2) ∨
(∃j≥a. j ≤ b - 1 ∧ semantics_mltl (drop j π) F1 ∧
(∀k. a ≤ k ∧ k ≤ j ⟶ semantics_mltl (drop k π) F2)))"
if i_prop: "(⋀i. (a - 1 ≤ i ∧ i ≤ b - 1) ⟹
semantics_mltl (drop i (drop 1 π)) F2 ∨
(∃j. a - 1 ≤ j ∧ j < i ∧ semantics_mltl (drop j (drop 1 π)) F1))"
proof -
{assume contra: "¬(∀i. a ≤ i ∧ i ≤ b ⟶ semantics_mltl (drop i π) F2)"
then have exi: "∃i. a ≤ i ∧ i ≤ b ∧ ¬ (semantics_mltl (drop i π) F2)"
by blast
then obtain i where least_exi:
"i = (LEAST j. a ≤ j ∧j ≤ b ∧ ¬ (semantics_mltl (drop j π) F2))"
by blast
then have least_prop1: "a ≤ i ∧i ≤ b ∧ ¬ (semantics_mltl (drop i π) F2)"
by (metis (no_types, lifting) LeastI ‹∃i≥a. i ≤ b ∧ ¬ semantics_mltl (drop i π) F2›)
have least_prop2: "(semantics_mltl (drop k π) F2)" if k: "a ≤ k ∧ k < i" for k
using Least_le exi least_exi k
by (smt (z3) linorder_not_less order.asym order_le_less_trans)
have i_bound: "a - 1 ≤ i - 1 ∧ i - 1 ≤ b - 1"
using least_prop1 * by auto
have "¬ (semantics_mltl (drop (i - 1) (drop 1 π)) F2)"
using least_prop1 * by auto
then have "∃j. a - 1 ≤ j ∧ j < i-1 ∧ semantics_mltl (drop (j+1) π) F1"
using i_prop[OF i_bound] by simp
then obtain j where " a - 1 ≤ j ∧ j < i-1 ∧ semantics_mltl (drop (j+1) π) F1"
by auto
then have "j+1 ≥ a ∧ j+1 ≤ b - 1 ∧ semantics_mltl (drop (j+1) π) F1 ∧
(∀k. a ≤ k ∧ k ≤ (j+1) ⟶ semantics_mltl (drop k π) F2)"
using least_prop2 least_prop1
by (smt (z3) Suc_eq_plus1 Suc_leI le_diff_conv le_imp_less_Suc less_diff_conv order_less_le_trans)
then have "(∃j≥a. j ≤ b - 1 ∧ semantics_mltl (drop j π) F1 ∧
(∀k. a ≤ k ∧ k ≤ j ⟶ semantics_mltl (drop k π) F2))"
by blast
}
then show ?thesis by blast
qed
have "(∀i. (a - 1 ≤ i ∧ i ≤ b - 1) ⟶
semantics_mltl (drop i (drop 1 π)) F2 ∨
(∃j. a - 1 ≤ j ∧ j < i ∧ semantics_mltl (drop j (drop 1 π)) F1)) =
((∀i. a ≤ i ∧ i ≤ b ⟶ semantics_mltl (drop i π) F2) ∨
(∃j≥a. j ≤ b - 1 ∧
semantics_mltl (drop j π) F1 ∧
(∀k. a ≤ k ∧ k ≤ j ⟶ semantics_mltl (drop k π) F2)))"
using d1 d2 by blast
then have "(¬ (a - 1 < length (drop 1 π)) ∨
¬(∃i. (a - 1 ≤ i ∧ i ≤ b - 1) ∧
¬ semantics_mltl (drop i (drop 1 π)) F2 ∧
(∀j. a - 1 ≤ j ∧ j < i ⟶ ¬ semantics_mltl (drop j (drop 1 π)) F1))) =
(length π ≤ a ∨
(∀i. a ≤ i ∧ i ≤ b ⟶ semantics_mltl (drop i π) F2) ∨
(∃j≥a. j ≤ b - 1 ∧
semantics_mltl (drop j π) F1 ∧
(∀k. a ≤ k ∧ k ≤ j ⟶ semantics_mltl (drop k π) F2)))"
by (smt (verit) "*" One_nat_def Suc_leI assms(1) leD length_drop less_diff_iff linorder_not_less order_less_imp_le)
then have "(¬ semantics_mltl (drop 1 π)
(Until_mltl (Not_mltl F1) (a - 1) (b - 1) (Not_mltl F2))) =
(length π ≤ a ∨
(∀i. a ≤ i ∧ i ≤ b ⟶ semantics_mltl (drop i π) F2) ∨
(∃j≥a. j ≤ b - 1 ∧
semantics_mltl (drop j π) F1 ∧
(∀k. a ≤ k ∧ k ≤ j ⟶ semantics_mltl (drop k π) F2)))"
unfolding semantics_mltl.simps
using "*" diff_le_mono by presburger
then have ?case unfolding formula_progression_len1.simps
semantics_mltl.simps using Release_mltl *
by auto
} moreover {assume * :"0=a ∧ a<b"
have d1: "(semantics_mltl π F2 ∧
(semantics_mltl π F1 ∨
(∀i. (0 ≤ i ∧ i ≤ b - 1) ⟶
semantics_mltl (drop (i+1) π) F2 ∨
(∃j. 0 ≤ j ∧ j < i ∧ semantics_mltl (drop (j+1) π) F1))))"
if all_i: "((∀i. 0 ≤ i ∧ i ≤ b ⟶ semantics_mltl (drop i π) F2) ∨
(∃j≥0. j ≤ b - 1 ∧
semantics_mltl (drop j π) F1 ∧
(∀k. 0 ≤ k ∧ k ≤ j ⟶ semantics_mltl (drop k π) F2)))"
proof -
have F2: "semantics_mltl π F2"
using all_i by auto
{assume **: "(∀i. 0 ≤ i ∧ i ≤ b ⟶ semantics_mltl (drop i π) F2)"
have "(semantics_mltl π F1 ∨
(∀i. (0 ≤ i ∧ i ≤ b - 1) ⟶
semantics_mltl (drop (i+1) π) F2 ∨
(∃j. 0 ≤ j ∧ j < i ∧ semantics_mltl (drop (j+1) π) F1)))"
using **
by (simp add: "*" Nat.le_diff_conv2 Suc_leI)
then have ?thesis using F2 by auto
} moreover {assume ** : " (∃j≥0. j ≤ b - 1 ∧
semantics_mltl (drop j π) F1 ∧
(∀k. 0 ≤ k ∧ k ≤ j ⟶ semantics_mltl (drop k π) F2))"
then obtain j where j_prop: "0≤ j ∧ j ≤ b - 1 ∧
semantics_mltl (drop j π) F1 ∧
(∀k. 0 ≤ k ∧ k ≤ j ⟶ semantics_mltl (drop k π) F2)"
by auto
{assume * :"j = 0"
then have "(semantics_mltl π F1 ∨
(∀i. (0 ≤ i ∧ i ≤ b - 1) ⟶
semantics_mltl (drop (i+1) π) F2 ∨
(∃j. 0 ≤ j ∧ j < i ∧ semantics_mltl (drop (j+1) π) F1)))"
using j_prop by simp
} moreover {assume * :"j > 0"
then have " (∀i. (0 ≤ i ∧ i ≤ b - 1) ⟶
semantics_mltl (drop (i+1) π) F2 ∨
(∃j. 0 ≤ j ∧ j < i ∧ semantics_mltl (drop (j+1) π) F1))"
using j_prop
by (metis Nat.le_imp_diff_is_add le0 less_diff_conv less_one linorder_le_less_linear nat_less_le)
}
ultimately have "(semantics_mltl π F1 ∨
(∀i. (0 ≤ i ∧ i ≤ b - 1) ⟶
semantics_mltl (drop (i+1) π) F2 ∨
(∃j. 0 ≤ j ∧ j < i ∧ semantics_mltl (drop (j+1) π) F1)))"
using j_prop by blast
then have ?thesis using F2 by auto
}
ultimately show ?thesis using all_i
by blast
qed
have d2: "((∀i. 0 ≤ i ∧ i ≤ b ⟶ semantics_mltl (drop i π) F2) ∨
(∃j≥0. j ≤ b - 1 ∧
semantics_mltl (drop j π) F1 ∧
(∀k. 0 ≤ k ∧ k ≤ j ⟶ semantics_mltl (drop k π) F2)))"
if all_i: "(semantics_mltl π F2 ∧
(semantics_mltl π F1 ∨
(∀i. (0 ≤ i ∧ i ≤ b - 1) ⟶
semantics_mltl (drop (i+1) π) F2 ∨
(∃j. 0 ≤ j ∧ j < i ∧ semantics_mltl (drop (j+1) π) F1))))"
proof -
have F2: "semantics_mltl π F2"
using all_i by auto
{assume **: "semantics_mltl π F1"
then have "0 ≤ b - 1 ∧
semantics_mltl (drop 0 π) F1 ∧
(∀k. 0 ≤ k ∧ k ≤ 0 ⟶ semantics_mltl (drop k π) F2)"
using F2 * by simp
then have ?thesis by blast
} moreover {assume **: " (∀i. (0 ≤ i ∧ i ≤ b - 1) ⟶
semantics_mltl (drop (i+1) π) F2 ∨
(∃j. 0 ≤ j ∧ j < i ∧ semantics_mltl (drop (j+1) π) F1))"
{assume contra: "∃i. 0 ≤ i ∧ i ≤ b ∧ ¬ (semantics_mltl (drop i π) F2) ∧
¬(∃j≥0. j ≤ b - 1 ∧
semantics_mltl (drop j π) F1 ∧
(∀k. 0 ≤ k ∧ k ≤ j ⟶ semantics_mltl (drop k π) F2))"
then have "¬(∃j≥0. j ≤ b - 1 ∧
semantics_mltl (drop j π) F1 ∧
(∀k. 0 ≤ k ∧ k ≤ j ⟶ semantics_mltl (drop k π) F2))"
by meson
then have all_j: "(⋀j. (j ≥ 0 ∧ j ≤ b - 1) ⟹
¬ (semantics_mltl (drop j π) F1) ∨
(∃k. 0 ≤ k ∧ k ≤ j ∧ ¬(semantics_mltl (drop k π) F2)))"
by blast
obtain i where least_i: "i = (LEAST j. 0 ≤ j ∧ j ≤ b ∧ ¬ (semantics_mltl (drop j π) F2))"
using contra
by auto
then have least_i1:"0 ≤ i ∧ i ≤ b ∧ ¬ (semantics_mltl (drop i π) F2)"
using least_i
by (metis (no_types, lifting) LeastI contra)
have least_i2: "⋀j. 0 ≤ j ∧ j < i ⟶ (semantics_mltl (drop j π) F2)"
using least_i
by (smt (z3) Least_le least_i1 dual_order.strict_iff_order dual_order.trans linorder_not_less)
{assume i_zer: "i = 0"
then have "False"
using F2 least_i1
by auto
} moreover {assume i_zer: "i > 0"
then have i_bound: "0 ≤ i-1 ∧ i-1 ≤ b - 1"
using least_i1
by auto
then have "semantics_mltl (drop i π) F2 ∨ (∃j≥0. j < i-1 ∧ semantics_mltl (drop (j + 1) π) F1)"
using **
by (metis One_nat_def Suc_leI i_zer le_add_diff_inverse2)
then have "(∃j≥0. j < i - 1 ∧ semantics_mltl (drop (j + 1) π) F1)"
using least_i1 by auto
then obtain j where j_bounds: "j ≥ 0 ∧ j < i - 1 ∧ semantics_mltl (drop (j + 1) π) F1"
by auto
have "(∃k. 0 ≤ k ∧ k ≤ (j+1) ∧ ¬(semantics_mltl (drop k π) F2))"
using all_j j_bounds i_bound by auto
then obtain k where "0 ≤ k ∧ k ≤ (j+1) ∧ ¬(semantics_mltl (drop k π) F2)"
by blast
then have "False"
using j_bounds least_i2 i_bound ** F2
by (meson less_diff_conv order_le_less_trans)
}
ultimately have "False" by auto
}
then have ?thesis by blast
}
ultimately show ?thesis using all_i by blast
qed
have "(semantics_mltl π F2 ∧
(semantics_mltl π F1 ∨
(∀i. (0 ≤ i ∧ i ≤ b - 1) ⟶
semantics_mltl (drop (i+1) π) F2 ∨
(∃j. 0 ≤ j ∧ j < i ∧ semantics_mltl (drop (j+1) π) F1)))) =
((∀i. 0 ≤ i ∧ i ≤ b ⟶ semantics_mltl (drop i π) F2) ∨
(∃j≥0. j ≤ b - 1 ∧
semantics_mltl (drop j π) F1 ∧
(∀k. 0 ≤ k ∧ k ≤ j ⟶ semantics_mltl (drop k π) F2)))"
using d1 d2 by blast
then have "(¬ (¬ semantics_mltl π F2 ∨
¬ semantics_mltl π F1 ∧
0 ≤ b - 1 ∧
0 < length (drop 1 π) ∧
(∃i. (0 ≤ i ∧ i ≤ b - 1) ∧
¬ semantics_mltl (drop i (drop 1 π)) F2 ∧
(∀j. 0 ≤ j ∧ j < i ⟶ ¬ semantics_mltl (drop j (drop 1 π)) F1)))) =
((∀i. 0 ≤ i ∧ i ≤ b ⟶ semantics_mltl (drop i π) F2) ∨
(∃j≥0. j ≤ b - 1 ∧
semantics_mltl (drop j π) F1 ∧
(∀k. 0 ≤ k ∧ k ≤ j ⟶ semantics_mltl (drop k π) F2)))"
using * assms(1) by auto
then have "(¬ semantics_mltl (drop 1 π)
(Or_mltl (Not_mltl (formula_progression_len1 F2 (π ! 0)))
(And_mltl (Not_mltl (formula_progression_len1 F1 (π ! 0)))
(Until_mltl (Not_mltl F1) 0 (b - 1) (Not_mltl F2))))) =
((∀i. 0 ≤ i ∧ i ≤ b ⟶ semantics_mltl (drop i π) F2) ∨
(∃j≥0. j ≤ b - 1 ∧
semantics_mltl (drop j π) F1 ∧
(∀k. 0 ≤ k ∧ k ≤ j ⟶ semantics_mltl (drop k π) F2)))"
unfolding semantics_mltl.simps using Release_mltl *
by auto
then have ?case using Release_mltl unfolding formula_progression_len1.simps
semantics_mltl.simps using Release_mltl *
by auto
}
moreover {assume * :"¬(0< a ∧ a≤ b) ∧ ¬ (0=a ∧ a<b)"
then have **: "a = b ∧ b = 0"
using Release_mltl(4) by auto
then have "semantics_mltl π F2 =
(length π ≤ a ∨
(∀i. 0 ≤ i ∧ i ≤ 0 ⟶ semantics_mltl (drop i π) F2))"
using assms(1) by auto
then have "semantics_mltl π F2 =
(length π ≤ a ∨
(∀i. 0 ≤ i ∧ i ≤ 0 ⟶ semantics_mltl (drop i π) F2) ∨
(∃j≥0. j ≤ 0 - 1 ∧
semantics_mltl (drop j π) F1 ∧
(∀k. a ≤ k ∧ k ≤ j ⟶ semantics_mltl (drop k π) F2)))"
using "**" by force
then have ?case unfolding formula_progression_len1.simps
semantics_mltl.simps using Release_mltl ** by auto
}
ultimately show ?case by blast
qed
text ‹ Theorem 2 ›
theorem satisfiability_preservation:
fixes φ::"'a mltl"
assumes "k ≥ 1"
assumes "k < length π"
assumes "intervals_welldef φ"
shows "semantics_mltl (drop k π) (formula_progression φ (take k π ))
⟷ semantics_mltl π φ"
using assms
proof (induct k arbitrary: π φ rule: less_induct)
case (less k)
{assume *: "k = 1"
then have "semantics_mltl (drop 1 π) (formula_progression_len1 φ (π ! 0))
⟷ semantics_mltl π φ"
using satisfiability_preservation_len1 less
by blast
then have ?case using * less unfolding formula_progression_len1.simps
by simp
} moreover {assume *: "k > 1"
let ?tr = "(drop (k-1) π)"
let ?fm = "formula_progression φ (take (k-1) π )"
let ?tr1 = "(drop k π)"
let ?fm1 = "formula_progression ?fm [π ! (k-1)]"
have "semantics_mltl ?tr ?fm ⟷ semantics_mltl π φ"
using less * by auto
have drop_id: "drop 1 (drop (k - 1) π) = ?tr1"
using *
by auto
have take_id: "take 1 (drop (k - 1) π) = [π ! (k-1)]"
using * less(3)
by (metis Cons_nth_drop_Suc One_nat_def diff_less dual_order.strict_trans less_numeral_extra(1) take0 take_Suc_Cons)
have ind_welldef: " intervals_welldef (formula_progression φ (take (k - 1) π))"
using less(4) formula_progression_well_definedness_preserved[of φ "(take (k - 1) π)"]
by blast
have "1 < length (drop (k - 1) π)"
using less * by auto
then have same_sem: "semantics_mltl ?tr ?fm ⟷ semantics_mltl ?tr1 ?fm1"
using less(1)[of 1 ?tr ?fm] * drop_id take_id ind_welldef
by auto
have "?fm1 = formula_progression φ (take k π )"
using formula_progression_decomposition[of "k-1" "take k π"] * less *
by simp
then have ?case
using same_sem
using ‹semantics_mltl (drop (k - 1) π) (formula_progression φ (take (k - 1) π)) = semantics_mltl π φ› by presburger
}
ultimately show ?case
using less
by auto
qed
paragraph ‹Counter example to Theorem 2 showing how the theorem can fail if
the trace length condition is removed.›
lemma theorem2_cexa:
fixes φ::"nat mltl"
assumes "k = 1"
assumes "π = [{1::nat}]"
assumes "φ = G⇩m [0,3] (Prop_mltl (1::nat))"
assumes "intervals_welldef φ"
shows "(drop k π) ⊨⇩m (formula_progression φ (take k π)) = True"
using assms unfolding semantics_mltl.simps by auto
value "(take 1 [{1::nat}])"
value "formula_progression (G⇩m [0,3] (Prop_mltl (1::nat))) (take 1 [{1::nat}])"
lemma theorem2_cexb:
fixes φ::"nat mltl"
assumes "π = [{1::nat}]"
assumes "φ = G⇩m [0,1] (Prop_mltl (1::nat))"
assumes "intervals_welldef φ"
shows "semantics_mltl π φ = False"
using assms unfolding semantics_mltl.simps assms
by auto
subsubsection ‹Theorem 3›
paragraph ‹Setup: Properties of Computation Length›
lemma complen_geq_1:
shows "complen_mltl φ ≥ 1"
apply (induction φ) by simp_all
text ‹ This is a key property that makes the base case of Theorem 3 work:
Constraining the computation length of the formula means that
the formula progression is either globally true or false.
This is a very strong structural property that lets us use the
inductive hypotheses in, e.g., the Or case and the Not case of
the base case of Theorem 3. ›
lemma complen_bounded_by_1:
assumes "intervals_welldef φ"
assumes "1 ≥ complen_mltl φ"
shows "(∀ξ. ξ ⊨⇩m(formula_progression_len1 φ π)) ∨
(∀ξ. ¬ (ξ ⊨⇩m (formula_progression_len1 φ π)))"
using assms
proof (induct φ arbitrary: π)
case True_mltl
then show ?case
by auto
next
case False_mltl
then show ?case by auto
next
case (Prop_mltl x)
then show ?case by simp
next
case (Not_mltl φ)
then show ?case by auto
next
case (And_mltl φ1 φ2)
then show ?case by auto
next
case (Or_mltl φ1 φ2)
then show ?case by auto
next
case (Future_mltl φ a b)
then show ?case
using One_nat_def add_diff_cancel_left' add_diff_cancel_right' complen_geq_one complen_mltl.simps(8) formula_progression_len1.simps(10) le_add2 less_numeral_extra(3) nle_le order_less_le_trans plus_1_eq_Suc
by (metis intervals_welldef.simps(7))
next
case (Global_mltl φ a b)
then show ?case
by (metis (no_types, lifting) One_nat_def add_diff_cancel_left' add_diff_cancel_right' complen_geq_one complen_mltl.simps(7) formula_progression_len1.simps(10) formula_progression_len1.simps(4) formula_progression_len1.simps(9) intervals_welldef.simps(8) le_add2 less_numeral_extra(3) nle_le plus_1_eq_Suc semantics_mltl.simps(4) zero_le)
next
case (Until_mltl φ1 a b φ2)
have "max (complen_mltl φ1 - 1) (complen_mltl φ2) ≥ 1"
using complen_geq_1
using max.coboundedI2 by blast
then have "a = 0 ∧ b = 0"
using Until_mltl(4) complen_geq_1 unfolding complen_mltl.simps
by (metis Until_mltl.prems(1) add_cancel_right_left add_leD2 complen_mltl.simps(10) intervals_welldef.simps(9) le_antisym le_zero_eq)
then show ?case
using Until_mltl
by simp
next
case (Release_mltl φ1 a b φ2)
have "max (complen_mltl φ1 - 1) (complen_mltl φ2) ≥ 1"
using complen_geq_1
using max.coboundedI2 by blast
then have "a = 0 ∧ b = 0"
using Release_mltl(4) unfolding complen_mltl.simps
by (metis Release_mltl.prems(1) add_diff_cancel_right' add_leD2 diff_is_0_eq' intervals_welldef.simps(10) le_antisym le_zero_eq)
then show ?case
using Release_mltl
by simp
qed
lemma complen_temporal_props:
shows "(complen_mltl (F⇩m [a,b] φ) = 1 ⟹ (b = 0))"
"(complen_mltl (G⇩m [a,b] φ) = 1 ⟹ (b = 0))"
"(complen_mltl (φ1 U⇩m [a,b] φ2) = 1 ⟹ (b = 0))"
"(complen_mltl (φ1 R⇩m [a,b] φ2) = 1 ⟹ (b = 0))"
proof -
assume "complen_mltl (F⇩m [a,b] φ) = 1"
then show "b = 0"
unfolding complen_mltl.simps using complen_geq_1
by (metis add_le_same_cancel2 le_zero_eq)
next assume "complen_mltl (G⇩m [a,b] φ) = 1"
then show "b = 0"
unfolding complen_mltl.simps using complen_geq_1
by (metis add_le_same_cancel2 le_zero_eq)
next assume "complen_mltl (φ1 U⇩m [a,b] φ2) = 1"
then show "b = 0"
unfolding complen_mltl.simps using complen_geq_1
by (metis add_le_same_cancel2 le_zero_eq max.coboundedI2)
next assume "complen_mltl (φ1 R⇩m [a,b] φ2) = 1"
then show "b = 0"
unfolding complen_mltl.simps using complen_geq_1
by (metis One_nat_def add_is_1 max_nat.eq_neutr_iff not_one_le_zero)
qed
lemma complen_one_implies_one_base:
assumes "intervals_welldef φ"
assumes "complen_mltl φ = 1"
shows "complen_mltl (formula_progression_len1 φ k) = 1"
using assms
proof (induct φ)
case True_mltl
then show ?case by simp
next
case False_mltl
then show ?case by simp
next
case (Prop_mltl x)
then show ?case by simp
next
case (Not_mltl φ)
then show ?case by simp
next
case (And_mltl φ1 φ2)
then show ?case using complen_geq_1
unfolding formula_progression_len1.simps
by (metis (full_types) complen_mltl.simps(5) intervals_welldef.simps(5) max.absorb1 max_def)
next
case (Or_mltl φ1 φ2)
then show ?case using complen_geq_1
unfolding formula_progression_len1.simps intervals_welldef.simps(6)
by (metis complen_mltl.simps(6) max.cobounded1 max.cobounded2 nle_le)
next
case (Future_mltl a b φ)
then have "a = 0 ∧ b = 0"
using complen_temporal_props(1)[of a b φ]
unfolding intervals_welldef.simps by simp
then show ?case
by (metis Future_mltl.hyps Future_mltl.prems(1) Future_mltl.prems(2) One_nat_def add_diff_cancel_left' add_diff_cancel_right' complen_mltl.simps(8) formula_progression_len1.simps(10) intervals_welldef.simps(7) less_numeral_extra(3) plus_1_eq_Suc)
next
case (Global_mltl a b φ)
then have "a = 0 ∧ b = 0"
using complen_temporal_props(2)[of a b φ]
unfolding intervals_welldef.simps by simp
then show ?case
using Global_mltl.hyps Global_mltl.prems(1) Global_mltl.prems(2) by auto
next
case (Until_mltl φ1 a b φ2)
then have "a = 0 ∧ b = 0"
using complen_temporal_props(3)[of φ1 a b φ2]
unfolding intervals_welldef.simps by simp
then show ?case
by (metis One_nat_def Until_mltl.hyps(2) Until_mltl.prems(1) Until_mltl.prems(2) add_diff_cancel_left' add_diff_cancel_right' complen_geq_1 complen_mltl.simps(10) formula_progression_len1.simps(7) intervals_welldef.simps(9) le_antisym less_numeral_extra(3) max.bounded_iff plus_1_eq_Suc)
next
case (Release_mltl φ1 a b φ2)
then have "a = 0 ∧ b = 0"
using complen_temporal_props(4)[of φ1 a b φ2]
unfolding intervals_welldef.simps by simp
then show ?case
by (metis (no_types, lifting) One_nat_def Release_mltl.hyps(2) Release_mltl.prems(1) Release_mltl.prems(2) add_diff_cancel_left' add_diff_cancel_right' complen_geq_1 complen_mltl.simps(4) complen_mltl.simps(9) formula_progression_len1.simps(4) formula_progression_len1.simps(7) formula_progression_len1.simps(8) intervals_welldef.simps(10) less_numeral_extra(3) max_def plus_1_eq_Suc)
qed
lemma complen_one_implies_one:
assumes "intervals_welldef φ"
assumes "complen_mltl φ = 1"
shows "complen_mltl (formula_progression φ π) = 1"
using assms
proof (induct "length π" arbitrary: π φ)
case 0
then show ?case by auto
next
case (Suc x)
{assume *: "x = 0"
then have ?case
using complen_one_implies_one_base
Suc
by (metis One_nat_def formula_progression.elims)
} moreover {assume *: "x > 0"
then have "complen_mltl (formula_progression (formula_progression_len1 φ (π ! 0))
(drop 1 π)) = 1"
using complen_one_implies_one_base[OF Suc(3) Suc(4), of "π ! 0"] Suc(1)[of "(drop 1 π)" "formula_progression_len1 φ (π ! 0)"]
formula_progression_well_definedness_preserved_len1[of φ "π ! 0"]
by (metis Suc.hyps(2) Suc.prems(1) diff_Suc_1 length_drop)
then have ?case
using formula_progression.simps[of φ π] using Suc *
by auto
}
ultimately show ?case by blast
qed
lemma formula_progression_decreases_complen_base:
assumes "intervals_welldef φ"
shows "complen_mltl φ = 1 ∨ complen_mltl (formula_progression_len1 φ k) ≤ complen_mltl φ - 1"
using assms
proof (induct φ)
case True_mltl
then show ?case
by simp
next
case False_mltl
then show ?case by simp
next
case (Prop_mltl x)
then show ?case by simp
next
case (Not_mltl φ)
then show ?case by simp
next
case (And_mltl φ1 φ2)
{assume * :"complen_mltl φ1 = 1"
{assume ** :"complen_mltl φ2 = 1"
then have ?case
unfolding complen_mltl.simps using *
by auto
} moreover {assume ** : "complen_mltl φ2 >1 ∧ complen_mltl (formula_progression_len1 φ2 k) ≤ complen_mltl φ2 - 1"
then have ?case
unfolding complen_mltl.simps formula_progression_len1.simps using * complen_one_implies_one_base
by (metis And_mltl.prems complen_geq_1 intervals_welldef.simps(5) max_def)
}
ultimately have ?case
using And_mltl by fastforce
}
moreover {assume * : "complen_mltl φ1 > 1 ∧ complen_mltl (formula_progression_len1 φ1 k) ≤ complen_mltl φ1 - 1"
{assume ** :"complen_mltl φ2 = 1"
then have ?case
unfolding complen_mltl.simps using *
by (metis (no_types, lifting) And_mltl.prems complen_geq_1 complen_mltl.simps(5) complen_one_implies_one_base formula_progression_len1.simps(5) intervals_welldef.simps(5) max.absorb1)
} moreover {assume ** : "complen_mltl φ2 >1 ∧ complen_mltl (formula_progression_len1 φ2 k) ≤ complen_mltl φ2 - 1"
then have ?case
unfolding complen_mltl.simps formula_progression_len1.simps using * complen_one_implies_one_base
by (smt (z3) Nat.le_diff_conv2 complen_geq_1 max.coboundedI2 max.commute max_def)
}
ultimately have ?case using And_mltl
by (metis complen_geq_1 intervals_welldef.simps(5) order_le_imp_less_or_eq)
}
ultimately show ?case using And_mltl
by (metis complen_geq_1 intervals_welldef.simps(5) order_le_imp_less_or_eq)
next
case (Or_mltl φ1 φ2)
{assume * :"complen_mltl φ1 = 1"
{assume ** :"complen_mltl φ2 = 1"
then have ?case
unfolding complen_mltl.simps using *
by auto
} moreover {assume ** : "complen_mltl φ2 >1 ∧ complen_mltl (formula_progression_len1 φ2 k) ≤ complen_mltl φ2 - 1"
then have ?case
unfolding complen_mltl.simps formula_progression_len1.simps using * complen_one_implies_one_base
by (metis Or_mltl.prems complen_geq_1 intervals_welldef.simps(6) max_def)
}
ultimately have ?case
using Or_mltl by fastforce
}
moreover {assume * : "complen_mltl φ1 > 1 ∧ complen_mltl (formula_progression_len1 φ1 k) ≤ complen_mltl φ1 - 1"
{assume ** :"complen_mltl φ2 = 1"
then have ?case
unfolding complen_mltl.simps using *
by (metis (no_types, lifting) Or_mltl.prems complen_geq_1 complen_mltl.simps(6) complen_one_implies_one_base formula_progression_len1.simps(6) intervals_welldef.simps(6) max.absorb1)
} moreover {assume ** : "complen_mltl φ2 >1 ∧ complen_mltl (formula_progression_len1 φ2 k) ≤ complen_mltl φ2 - 1"
then have ?case
unfolding complen_mltl.simps formula_progression_len1.simps using * complen_one_implies_one_base
by (smt (z3) Nat.le_diff_conv2 complen_geq_1 max.coboundedI2 max.commute max_def)
}
ultimately have ?case using Or_mltl
by (metis complen_geq_1 intervals_welldef.simps(6) order_le_imp_less_or_eq)
}
ultimately show ?case using Or_mltl
by (metis complen_geq_1 intervals_welldef.simps(6) order_le_imp_less_or_eq)
next
case (Future_mltl a b φ)
{assume *: "complen_mltl φ = 1"
have iwd: "intervals_welldef φ"
using Future_mltl(2) by simp
have a_leq_b: "a≤b"
using Future_mltl
by auto
{assume **: "b = 0"
then have ?case
using * complen_one_implies_one_base[OF iwd *]
unfolding complen_mltl.simps by auto }
moreover {assume **: "b > 0"
have complen_not_dec: "complen_mltl (formula_progression_len1 φ p) = 1" for p
using complen_one_implies_one_base[OF iwd *] by auto
{assume ***: " 0 = a"
then have "(formula_progression_len1 (Future_mltl a b φ) k)
= (Or_mltl (formula_progression_len1 φ k) (Future_mltl 0 (b - 1) φ))"
unfolding formula_progression_len1.simps
using ** * by auto
then have "complen_mltl (formula_progression_len1 (Future_mltl a b φ) k) = b"
using * complen_not_dec **
by auto
then have ?case unfolding complen_mltl.simps using *
by simp
} moreover {assume ***: "a > 0"
then have "(formula_progression_len1 (Future_mltl a b φ) k)
= Future_mltl (a - 1) (b - 1) φ"
unfolding formula_progression_len1.simps
using ** * a_leq_b
by auto
then have "complen_mltl (formula_progression_len1 (Future_mltl a b φ) k)
= b"
using * **
by simp
then have ?case unfolding complen_mltl.simps using *
by auto
}
ultimately have ?case
by blast
}
ultimately have ?case
by blast
} moreover
{assume *:"complen_mltl (formula_progression_len1 φ k) ≤ complen_mltl φ - 1"
then have ?case unfolding complen_mltl.simps formula_progression_len1.simps
by auto
}
ultimately show ?case
using Future_mltl by fastforce
next
case (Global_mltl a b φ)
have a_leq_b: "a≤b"
using Global_mltl
by auto
{assume *: "complen_mltl φ = 1"
have iwd: "intervals_welldef φ"
using Global_mltl(2) by simp
{assume **: "b = 0"
then have ?case
using * complen_one_implies_one_base[OF iwd *]
unfolding complen_mltl.simps by auto
}
moreover {assume **: "b > 0"
have complen_1: "complen_mltl (Future_mltl (a - 1) (b - 1) (Not_mltl φ)) ≤ b"
unfolding complen_mltl.simps using * **
by auto
have complen_2: "complen_mltl (Or_mltl (Not_mltl (formula_progression_len1 φ k))
(Future_mltl 0 (b - 1) (Not_mltl φ))) ≤ b"
unfolding complen_mltl.simps using * ** complen_one_implies_one_base[OF iwd *]
by simp
then have "complen_mltl (formula_progression_len1 (Future_mltl a b (Not_mltl φ)) k) ≤ b"
unfolding formula_progression_len1.simps
using complen_1 complen_2 ** a_leq_b by simp
then have "complen_mltl (Not_mltl (formula_progression_len1 (Future_mltl a b (Not_mltl φ)) k)) ≤ b + complen_mltl φ - 1"
using complen_one_implies_one_base[OF iwd *]
unfolding complen_mltl.simps using * by auto
then have ?case
using formula_progression_len1.simps(9)
by simp
}
ultimately have ?case
by blast
} moreover
{assume *:"complen_mltl (formula_progression_len1 φ k) ≤ complen_mltl φ - 1"
then have ?case unfolding complen_mltl.simps formula_progression_len1.simps
by auto
}
ultimately show ?case
using Global_mltl by fastforce
next
case (Until_mltl φ1 a b φ2)
{assume *: "complen_mltl φ1 = 1 ∧ complen_mltl φ2 = 1"
{assume **: "b = 0"
then have ?case
unfolding complen_mltl.simps formula_progression_len1.simps
using * by auto
} moreover {assume **: "b > 0"
then have ?case
unfolding complen_mltl.simps formula_progression_len1.simps
using *
by (smt (verit) Nat.diff_diff_right Until_mltl(3) complen_mltl.simps(10) complen_mltl.simps(5) complen_mltl.simps(6) complen_one_implies_one_base diff_is_0_eq' intervals_welldef.simps(9) le_add_diff_inverse2 le_less le_simps(3) minus_nat.diff_0 nat_minus_add_max plus_1_eq_Suc zero_less_one_class.zero_le_one)
}
ultimately have ?case
by blast
} moreover {assume *: "complen_mltl φ1 = 1 ∧ complen_mltl φ2 > 1 ∧ complen_mltl (formula_progression_len1 φ2 k) ≤ complen_mltl φ2 - 1"
{assume **: "b = 0"
then have ?case
unfolding complen_mltl.simps formula_progression_len1.simps
using * by auto
} moreover {assume **: "b > 0"
{assume ***: "0 < a ∧ a ≤ b"
then have "complen_mltl
( Until_mltl φ1 (a - 1) (b - 1) φ2)
≤ b + max (complen_mltl φ1 - 1) (complen_mltl φ2) - 1"
using * ** by simp
} moreover {assume ***: "0 = a ∧ a < b"
have lt1: " (complen_mltl (formula_progression_len1 φ2 k))
≤ b + max (complen_mltl φ1 - 1) (complen_mltl φ2) - 1"
using * ** by auto
have complen_not_dec: "complen_mltl (formula_progression_len1 φ1 k) = 1"
using * complen_one_implies_one_base[of φ1] Until_mltl(3)
unfolding intervals_welldef.simps by blast
have lt2: "(max 1 (b - 1 + max 0 (complen_mltl φ2)))
≤ b + max 0 (complen_mltl φ2) - 1"
using * ** by auto
then have lt2: "(max (complen_mltl (formula_progression_len1 φ1 k))
(b - 1 + max (complen_mltl φ1 - 1) (complen_mltl φ2)))
≤ b + max (complen_mltl φ1 - 1) (complen_mltl φ2) - 1"
using * complen_not_dec by simp
have "complen_mltl
(Or_mltl (formula_progression_len1 φ2 k)
(And_mltl (formula_progression_len1 φ1 k)
(Until_mltl φ1 0 (b - 1) φ2)))
≤ b + max (complen_mltl φ1 - 1) (complen_mltl φ2) - 1"
unfolding complen_mltl.simps formula_progression_len1.simps
using lt1 lt2
using max.boundedI by blast
}
ultimately have ?case
unfolding complen_mltl.simps formula_progression_len1.simps
using * by auto
}
ultimately have ?case
by blast
} moreover {assume *: "complen_mltl φ2 = 1 ∧ complen_mltl φ1 > 1 ∧ complen_mltl (formula_progression_len1 φ1 k) ≤ complen_mltl φ1 - 1"
{assume **: "b = 0"
then have ?case
unfolding complen_mltl.simps formula_progression_len1.simps
using *
using Until_mltl.prems complen_one_implies_one_base by force
}
moreover {assume **: "b > 0"
{assume ***: "0 < a ∧ a ≤ b"
then have "b + max (complen_mltl φ1 - 1) (complen_mltl φ2) = 1 ∨
complen_mltl
(Until_mltl φ1 (a - 1) (b - 1) φ2)
≤ b + max (complen_mltl φ1 - 1) (complen_mltl φ2) - 1"
using * ** unfolding complen_mltl.simps
by (metis le_refl less_one ordered_cancel_comm_monoid_diff_class.add_diff_assoc2 verit_comp_simplify1(3))
then have ?case
using ***
by auto
} moreover {assume ***: "0 = a ∧ a < b"
then have " b + max (complen_mltl φ1 - 1) (complen_mltl φ2) = 1 ∨
complen_mltl
(Or_mltl (formula_progression_len1 φ2 k)
(And_mltl (formula_progression_len1 φ1 k)
(Until_mltl φ1 0 (b - 1) φ2)))
≤ b + max (complen_mltl φ1 - 1) (complen_mltl φ2) - 1"
using * ** unfolding complen_mltl.simps formula_progression_len1.simps
by (smt (verit) Nat.add_diff_assoc2 One_nat_def Until_mltl.prems dual_order.eq_iff complen_one_implies_one_base intervals_welldef.simps(9) leD le_add2 max.bounded_iff max_def not_less_eq_eq)
then have ?case
using ***
by auto
}
ultimately have ?case
using *
using "**" Until_mltl.prems intervals_welldef.simps(9) zero_less_iff_neq_zero by blast
}
ultimately have ?case
by blast
} moreover {assume *: "complen_mltl φ1 > 1 ∧ complen_mltl φ2 > 1 ∧ complen_mltl (formula_progression_len1 φ1 k) ≤ complen_mltl φ1 - 1 ∧ complen_mltl (formula_progression_len1 φ2 k) ≤ complen_mltl φ2 - 1"
{assume **: "b = 0"
then have ?case unfolding complen_mltl.simps formula_progression_len1.simps
using *
by (smt (verit, ccfv_threshold) add.commute add_diff_cancel_right' complen_geq_1 diff_diff_left le_zero_eq less_numeral_extra(3) max.cobounded2 nat_minus_add_max order.trans ordered_cancel_comm_monoid_diff_class.add_diff_assoc2)
} moreover {assume **: "b > 0"
{assume ***: "0 < a ∧ a ≤ b"
then have "b + max (complen_mltl φ1 - 1) (complen_mltl φ2) = 1 ∨
complen_mltl
(Until_mltl φ1 (a - 1) (b - 1) φ2)
≤ b + max (complen_mltl φ1 - 1) (complen_mltl φ2) - 1"
using * ** unfolding complen_mltl.simps
by (metis le_refl less_one ordered_cancel_comm_monoid_diff_class.add_diff_assoc2 verit_comp_simplify1(3))
then have ?case
using ***
by auto
} moreover {assume ***: "0 = a ∧ a < b"
then have " b + max (complen_mltl φ1 - 1) (complen_mltl φ2) = 1 ∨
complen_mltl
(Or_mltl (formula_progression_len1 φ2 k)
(And_mltl (formula_progression_len1 φ1 k)
(Until_mltl φ1 0 (b - 1) φ2)))
≤ b + max (complen_mltl φ1 - 1) (complen_mltl φ2) - 1"
using * ** unfolding complen_mltl.simps formula_progression_len1.simps
using less_or_eq_imp_le by fastforce
then have ?case
using ***
by auto
}
ultimately have ?case
using *
using "**" Until_mltl.prems intervals_welldef.simps(9) zero_less_iff_neq_zero by blast
}
ultimately have ?case
by blast
}
ultimately show ?case using Until_mltl
by (metis antisym_conv2 complen_geq_1 intervals_welldef.simps(9))
next
case (Release_mltl φ1 a b φ2)
{assume *: "complen_mltl φ1 = 1 ∧ complen_mltl φ2 = 1"
{assume **: "b = 0"
then have "b + max (complen_mltl φ1 - 1) (complen_mltl φ2) = 1"
using * by auto
then have ?case
unfolding complen_mltl.simps formula_progression_len1.simps
by auto
} moreover {assume **: "b > 0"
{assume ***: "0 < a ∧ a ≤ b"
then have "complen_mltl
(Until_mltl (Not_mltl φ1) (a - 1) (b - 1) (Not_mltl φ2))
≤ b + max (complen_mltl φ1 - 1) (complen_mltl φ2) - 1"
using * unfolding complen_mltl.simps formula_progression_len1.simps
by auto
then have ?case
using *** by auto
} moreover {assume ***: "0 = a ∧ a < b"
have complen_1:"(complen_mltl (formula_progression_len1 φ2 k)) = 1 ∧ (complen_mltl (formula_progression_len1 φ1 k)) = 1"
using * Release_mltl(3) unfolding intervals_welldef.simps
using complen_one_implies_one_base by blast
have "max 1 (max 1 (b - 1 + max (complen_mltl φ1 - 1) (complen_mltl φ2)))
≤ b + max (complen_mltl φ1 - 1) (complen_mltl φ2) - 1"
using *** unfolding complen_mltl.simps using *
by auto
then have "complen_mltl
(Or_mltl (Not_mltl (formula_progression_len1 φ2 k))
(And_mltl
(Not_mltl (formula_progression_len1 φ1 k))
(Until_mltl (Not_mltl φ1) 0 (b - 1) (Not_mltl φ2))))
≤ b + max (complen_mltl φ1 - 1) (complen_mltl φ2) - 1"
unfolding complen_mltl.simps using * complen_1
by auto
then have ?case
using *** *
unfolding complen_mltl.simps formula_progression_len1.simps
by auto
}
ultimately have ?case
unfolding complen_mltl.simps formula_progression_len1.simps
using **
using Release_mltl.prems intervals_welldef.simps(10) zero_less_iff_neq_zero by blast
}
ultimately have ?case
by blast
} moreover {assume *: "complen_mltl φ1 = 1 ∧ complen_mltl φ2 > 1 ∧ complen_mltl (formula_progression_len1 φ2 k) ≤ complen_mltl φ2 - 1"
{assume **: "b = 0"
then have "complen_mltl
(Not_mltl (formula_progression_len1 φ2 k))
≤ b + max (complen_mltl φ1 - 1) (complen_mltl φ2) - 1"
unfolding complen_mltl.simps
using * by auto
then have ?case
using ** unfolding complen_mltl.simps formula_progression_len1.simps
using * by auto
} moreover {assume **: "b > 0"
{assume ***: "0 < a ∧ a ≤ b"
then have "complen_mltl
(Until_mltl (Not_mltl φ1) (a - 1) (b - 1) (Not_mltl φ2))
≤ b + max (complen_mltl φ1 - 1) (complen_mltl φ2) - 1"
unfolding complen_mltl.simps
using * ** by simp
} moreover {assume ***: "0 = a ∧ a < b"
have complen_1: "(complen_mltl (formula_progression_len1 φ1 k)) = 1"
using complen_one_implies_one_base Release_mltl(3)
unfolding intervals_welldef.simps
using * by auto
have "max (complen_mltl (formula_progression_len1 φ2 k))
(max 1 (b - 1 + (complen_mltl φ2)))
≤ b + (complen_mltl φ2) - 1"
using * **
by fastforce
then have "max (complen_mltl (formula_progression_len1 φ2 k))
(max (complen_mltl (formula_progression_len1 φ1 k))
(b - 1 + max 0 (complen_mltl φ2)))
≤ b + max 0 (complen_mltl φ2) - 1"
using * complen_1
by auto
then have "complen_mltl
(Or_mltl (Not_mltl (formula_progression_len1 φ2 k))
(And_mltl
(Not_mltl (formula_progression_len1 φ1 k))
(Until_mltl (Not_mltl φ1) 0
(b - 1) (Not_mltl φ2))))
≤ b + max 0 (complen_mltl φ2) - 1"
using *
unfolding complen_mltl.simps formula_progression_len1.simps
by auto
then have "complen_mltl
(Or_mltl (Not_mltl (formula_progression_len1 φ2 k))
(And_mltl
(Not_mltl (formula_progression_len1 φ1 k))
(Until_mltl (Not_mltl φ1) 0
(b - 1) (Not_mltl φ2))))
≤ b + max (complen_mltl φ1 - 1) (complen_mltl φ2) - 1"
using * by auto
}
ultimately have ?case
unfolding formula_progression_len1.simps
using * ** by auto
}
ultimately have ?case
by blast
}
moreover {assume *: "complen_mltl φ2 = 1 ∧ complen_mltl φ1 > 1 ∧ complen_mltl (formula_progression_len1 φ1 k) ≤ complen_mltl φ1 - 1"
then have complen_fp_phi2: "complen_mltl (formula_progression_len1 φ2 k) = 1"
using complen_one_implies_one_base [of φ2]
Release_mltl(3) unfolding intervals_welldef.simps
by blast
{assume **: "b = 0"
then have "b + max (complen_mltl φ1 - 1) (complen_mltl φ2) = 1 ∨
complen_mltl (formula_progression_len1 φ2 k)
≤ b + max (complen_mltl φ1 - 1) (complen_mltl φ2) - 1"
using * complen_fp_phi2
by auto
then have "b + max (complen_mltl φ1 - 1) (complen_mltl φ2) = 1 ∨ complen_mltl
(Not_mltl (formula_progression_len1 φ2 k))
≤ b + max (complen_mltl φ1 - 1) (complen_mltl φ2) - 1"
unfolding complen_mltl.simps formula_progression_len1.simps
by blast
then have ?case using **
by auto
}
moreover {assume **: "b > 0"
{assume ***: "0 < a ∧ a ≤ b"
have "b + max (complen_mltl φ1 - 1) (complen_mltl φ2) = 1 ∨
complen_mltl
(Until_mltl (Not_mltl φ1) (a - 1) (b - 1) (Not_mltl φ2))
≤ b + max (complen_mltl φ1 - 1) (complen_mltl φ2) - 1"
unfolding complen_mltl.simps using **
by auto
then have ?case
using *** unfolding complen_mltl.simps formula_progression_len1.simps
by auto
} moreover {assume ***: "0 = a ∧ a < b"
have max_simp: "max (complen_mltl φ1 - 1) 1 = (complen_mltl φ1 - 1)"
using * by auto
have max_is: "max 1 (max (complen_mltl φ1 - 1) (b - 1 + complen_mltl φ1 - 1)) =
max (complen_mltl φ1 - 1) (b - 1 + complen_mltl φ1 - 1)"
using * by auto
have "max (complen_mltl φ1 - 1) (b - 1 + complen_mltl φ1 - 1)
≤ b + (complen_mltl φ1 - 1) - 1"
using * ** by auto
then have "max 1 (max (complen_mltl (formula_progression_len1 φ1 k))
(b - 1 + complen_mltl φ1 - 1))
≤ b + (complen_mltl φ1 - 1) - 1"
using max_is ** * by auto
then have "max 1 (max (complen_mltl (formula_progression_len1 φ1 k))
(b - 1 + max (complen_mltl φ1 - 1) 1))
≤ b + max (complen_mltl φ1 - 1) 1 - 1"
using max_simp
by auto
have "max (complen_mltl (formula_progression_len1 φ2 k))
(max (complen_mltl (formula_progression_len1 φ1 k))
(b - 1 + max (complen_mltl φ1 - 1) (complen_mltl φ2)))
≤ b + max (complen_mltl φ1 - 1) (complen_mltl φ2) - 1"
using * ** complen_fp_phi2
by auto
then have "complen_mltl
(Or_mltl (Not_mltl (formula_progression_len1 φ2 k))
(And_mltl (Not_mltl (formula_progression_len1 φ1 k))
(Until_mltl (Not_mltl φ1) 0 (b - 1) (Not_mltl φ2))))
≤ b + max (complen_mltl φ1 - 1) (complen_mltl φ2) - 1"
unfolding complen_mltl.simps
by auto
then have ?case
using *** unfolding complen_mltl.simps formula_progression_len1.simps
by auto
}
ultimately have ?case
using * **
using Release_mltl.prems intervals_welldef.simps(9) zero_less_iff_neq_zero
by fastforce
}
ultimately have ?case
by blast
} moreover {assume *: "complen_mltl φ1 > 1 ∧ complen_mltl φ2 > 1 ∧ complen_mltl (formula_progression_len1 φ1 k) ≤ complen_mltl φ1 - 1 ∧ complen_mltl (formula_progression_len1 φ2 k) ≤ complen_mltl φ2 - 1"
{assume **: "b = 0"
then have "complen_mltl (Not_mltl (formula_progression_len1 φ2 k))
≤ b + max (complen_mltl φ1 - 1) (complen_mltl φ2) - 1"
unfolding complen_mltl.simps formula_progression_len1.simps
using * by auto
then have ?case unfolding complen_mltl.simps formula_progression_len1.simps
using * **
by auto
} moreover {assume **: "b > 0"
{assume ***: "0 < a ∧ a ≤ b"
then have complen: "complen_mltl (Until_mltl (Not_mltl φ1) (a - 1) (b - 1) (Not_mltl φ2))
≤ b + max (complen_mltl φ1 - 1) (complen_mltl φ2) - 1"
using * ** unfolding complen_mltl.simps
by simp
have ?case
unfolding complen_mltl.simps formula_progression_len1.simps
using *** complen
by auto
} moreover {assume ***: "0 = a ∧ a < b"
have max_is: "max (complen_mltl φ1 - 1) (b - 1 + max (complen_mltl φ1 - 1) (complen_mltl φ2))
= (b - 1 + max (complen_mltl φ1 - 1) (complen_mltl φ2))"
using **
by simp
have "max (complen_mltl φ2 - 1) (b - 1 + max (complen_mltl φ1 - 1) (complen_mltl φ2))
≤ b + max (complen_mltl φ1 - 1) (complen_mltl φ2) - 1"
using *** by auto
then have "max (complen_mltl φ2 - 1)
(max (complen_mltl φ1 - 1)
(b - 1 + max (complen_mltl φ1 - 1) (complen_mltl φ2)))
≤ b + max (complen_mltl φ1 - 1) (complen_mltl φ2) - 1"
using max_is
by auto
then have "max (complen_mltl (formula_progression_len1 φ2 k))
(max (complen_mltl (formula_progression_len1 φ1 k))
(b - 1 + max (complen_mltl φ1 - 1) (complen_mltl φ2)))
≤ b + max (complen_mltl φ1 - 1) (complen_mltl φ2) - 1"
using *
by (smt (verit, best) max.absorb2 max.bounded_iff)
then have "complen_mltl (Or_mltl (Not_mltl (formula_progression_len1 φ2 k))
(And_mltl (Not_mltl (formula_progression_len1 φ1 k))
(Until_mltl (Not_mltl φ1) 0 (b - 1) (Not_mltl φ2))))
≤ b + max (complen_mltl φ1 - 1) (complen_mltl φ2) - 1"
using * ** unfolding complen_mltl.simps
by auto
then have ?case
unfolding formula_progression_len1.simps complen_mltl.simps
using ***
by auto
}
ultimately have ?case
using *
using "**" Release_mltl.prems intervals_welldef.simps(9) zero_less_iff_neq_zero
by simp
}
ultimately have ?case
by blast
}
ultimately show ?case using Release_mltl
using complen_geq_1[of φ1] complen_geq_1[of φ2]
by (metis antisym_conv2 intervals_welldef.simps(10))
qed
text ‹ Key helper lemma --- relates computation length and formula progression.
Intuitively, the formula progression usually decreases the computation length. ›
lemma formula_progression_decreases_complen:
assumes "intervals_welldef φ"
shows "complen_mltl φ = 1 ∨ complen_mltl (formula_progression φ π) = 1 ∨ complen_mltl (formula_progression φ π) ≤ complen_mltl φ - (length π)"
using assms
proof (induct "length π" arbitrary: π φ)
case 0
then show ?case by simp
next
case (Suc x)
{assume *: "Suc x = 1"
then have ?case
using formula_progression_decreases_complen_base
Suc by auto
} moreover {assume *: "Suc x > 1"
then have fp_is: "formula_progression φ π =
formula_progression (formula_progression_len1 φ (π ! 0))
(drop 1 π)"
using Suc(2) formula_progression.simps[of φ π]
by auto
have eo_base: "complen_mltl φ = 1 ∨
complen_mltl (formula_progression_len1 φ (π ! 0))
≤ complen_mltl φ - 1"
using formula_progression_decreases_complen_base[of φ "π ! 0"]
Suc(3) formula_progression_well_definedness_preserved_len1
by blast
{assume **: "complen_mltl φ = 1"
then have ?case
by auto
} moreover {assume **: "complen_mltl (formula_progression_len1 φ (π ! 0))
≤ complen_mltl φ - 1"
{assume *** : "complen_mltl (formula_progression_len1 φ (π ! 0)) = 1 "
then have "complen_mltl (formula_progression (formula_progression_len1 φ (π ! 0))
(drop 1 π)) = 1"
using complen_one_implies_one[of "formula_progression_len1 φ (π ! 0)"] formula_progression_well_definedness_preserved_len1[OF Suc(3), of "π ! 0"]
by blast
then have "complen_mltl (formula_progression φ π) = 1"
using Suc * formula_progression.simps
by auto
then have ?case
by auto
} moreover {assume ***: "complen_mltl
(formula_progression (formula_progression_len1 φ (π ! 0))
(drop 1 π)) =
1"
then have "complen_mltl (formula_progression φ π) = 1"
using Suc * formula_progression.simps
by auto
then have ?case
by auto
}
moreover {assume **: "complen_mltl (formula_progression (formula_progression_len1 φ (π ! 0))
(drop 1 π)) ≤ complen_mltl φ - length π"
then have "complen_mltl (formula_progression (formula_progression_len1 φ (π ! 0))
(drop 1 π)) ≤ complen_mltl φ - length π"
by blast
then have ?case
by auto
}
ultimately have ?case
using Suc(1)[of "drop 1 π" "formula_progression_len1 φ (π ! 0)"]
formula_progression_well_definedness_preserved_len1[OF Suc(3), of "π ! 0"]
by (smt (verit) "**" Suc.hyps(2) diff_Suc_1 diff_Suc_eq_diff_pred diff_le_mono le_trans length_drop) }
ultimately have ?case
using eo_base fp_is
by metis
}
ultimately show ?case by linarith
qed
paragraph ‹Base case›
lemma formula_progression_correctness_len1_helper:
fixes φ::"'a mltl"
assumes "length π = 1"
assumes "intervals_welldef φ"
assumes "length π ≥ complen_mltl φ"
shows "(semantic_equiv (formula_progression_len1 φ (π ! 0)) True_mltl) ⟷ semantics_mltl [π!0] φ"
using assms
proof -
show ?thesis using assms
proof (induction φ)
case True_mltl
then show ?case
by (simp add: semantic_equiv_def)
next
case False_mltl
then show ?case by (simp add: semantic_equiv_def)
next
case (Prop_mltl x)
then show ?case
by (simp add: semantic_equiv_def)
next
case (Not_mltl φ)
then have "semantic_equiv (formula_progression_len1 φ (π ! 0)) True_mltl =
semantics_mltl [π ! 0] φ"
by simp
then have "(∀ξ. semantics_mltl ξ (formula_progression_len1 φ (π ! 0)) =
True) = semantics_mltl [π ! 0] φ"
unfolding semantic_equiv_def
by (meson semantics_mltl.simps(1))
then show ?case unfolding semantics_mltl.simps formula_progression_len1.simps
unfolding semantic_equiv_def
using complen_bounded_by_1
using Not_mltl.prems(2) Not_mltl.prems(3) assms(1) by auto
next
case (And_mltl φ1 φ2)
then show ?case
using formula_progression_len1.simps(5) semantic_equiv_def semantics_mltl.simps(1) semantics_mltl.simps(5)
intervals_welldef.simps(5) complen_bounded_by_1
by (smt (verit, best) complen_geq_1 complen_mltl.simps(5) dual_order.eq_iff max_def)
next
case (Or_mltl φ1 φ2)
then have ind1: " semantic_equiv (formula_progression_len1 φ1 (π ! 0)) True_mltl = semantics_mltl [π ! 0] φ1"
by simp
have ind2: " semantic_equiv (formula_progression_len1 φ2 (π ! 0)) True_mltl = semantics_mltl [π ! 0] φ2"
using Or_mltl
by simp
show ?case
using complen_bounded_by_1 ind2 ind1
by (smt (verit, ccfv_SIG) Or_mltl.prems(2) Or_mltl.prems(3) assms(1) complen_mltl.simps(6) formula_progression_len1.simps(6) intervals_welldef.simps(6) max.bounded_iff semantic_equiv_def semantics_mltl.simps(1) semantics_mltl.simps(6))
next
case (Future_mltl a b φ)
then show ?case
by (smt (verit, del_insts) Cons_nth_drop_Suc add.commute add_diff_cancel_right' complen_geq_one complen_mltl.simps(8) drop0 formula_progression_len1.simps(10) intervals_welldef.simps(7) leD le_add2 le_imp_less_Suc le_zero_eq list.size(4) nle_le plus_1_eq_Suc semantics_mltl.simps(7))
next
case (Global_mltl a b φ)
then show ?case using One_nat_def add_diff_cancel_left' add_diff_cancel_right' complen_geq_one complen_mltl.simps(7) drop0 formula_progression_len1.simps(10) formula_progression_len1.simps(4) formula_progression_len1.simps(9) impossible_Cons intervals_welldef.simps(8) le_add2 le_zero_eq less_numeral_extra(3) nle_le plus_1_eq_Suc semantic_equiv_def semantics_mltl.simps(4) semantics_mltl.simps(8)
by (smt (verit))
next
case (Until_mltl φ1 a b φ2)
have "max (complen_mltl φ1 - 1) (complen_mltl φ2) ≥ 1"
using complen_geq_1
using max.coboundedI2 by blast
then have "a = 0 ∧ b = 0"
using Until_mltl(4) complen_geq_1 unfolding complen_mltl.simps
by (metis Until_mltl.prems(3) add_diff_cancel_right' assms(1) bot_nat_0.extremum complen_mltl.simps(10) diff_is_0_eq' intervals_welldef.simps(9) le_antisym)
then show ?case
using complen_bounded_by_1
using Until_mltl.IH(2) Until_mltl.prems(2) Until_mltl.prems(3) assms(1) by force
next
case (Release_mltl φ1 a b φ2)
have ind2: " semantic_equiv (formula_progression_len1 φ2 (π ! 0)) True_mltl = semantics_mltl [π ! 0] φ2"
using Release_mltl
by simp
have "max (complen_mltl φ1 - 1) (complen_mltl φ2) ≥ 1"
using complen_geq_1
using max.coboundedI2 by blast
then have "a = 0 ∧ b = 0"
using Release_mltl(4) complen_geq_1 unfolding complen_mltl.simps
by (metis Release_mltl.prems(3) add_diff_cancel_right' assms(1) bot_nat_0.extremum complen_mltl.simps(9) diff_is_0_eq' intervals_welldef.simps(10) le_antisym)
then have "formula_progression_len1 (Release_mltl φ1 a b φ2) (π ! 0) = Not_mltl ( Not_mltl (formula_progression_len1 φ2 (π ! 0)))"
unfolding formula_progression_len1.simps by auto
then show ?case using complen_bounded_by_1 ind2
by (smt (verit, ccfv_threshold) One_nat_def ‹a = 0 ∧ b = 0› add.commute diff_diff_cancel diff_is_0_eq' drop0 le_numeral_extra(3) list.size(3) list.size(4) not_not_equiv not_one_le_zero plus_1_eq_Suc semantic_equiv_def semantics_mltl.simps(10))
qed
qed
lemma formula_progression_correctness_len1:
fixes φ::"'a mltl"
assumes "length π = 1"
assumes "intervals_welldef φ"
assumes "length π ≥ complen_mltl φ"
shows "(formula_progression φ π ≡⇩m True⇩m) ⟷ π ⊨⇩m φ"
using assms formula_progression_correctness_len1_helper
by (metis Cons_nth_drop_Suc One_nat_def drop0 drop_eq_Nil2 formula_progression.simps le_numeral_extra(4) zero_less_one zero_neq_one)
paragraph ‹Top-Level Result and Corollary›
theorem formula_progression_correctness:
fixes φ::"'a mltl"
assumes "intervals_welldef φ"
assumes "length π ≥ complen_mltl φ"
shows "(formula_progression φ π ≡⇩m True⇩m) ⟷ π ⊨⇩m φ"
proof -
have len_pi_geq1: "length π ≥ 1"
using assms complen_geq_1[of φ]
by simp
{assume *: "length π = 1"
then have ?thesis
using formula_progression_correctness_len1 assms by blast
} moreover {assume *: "length π > 1"
let ?k = "length π - 1"
have t1: "semantics_mltl (drop ?k π) (formula_progression φ (take ?k π ))
⟷ semantics_mltl π φ"
using satisfiability_preservation assms * len_pi_geq1
by (metis One_nat_def Suc_leI Suc_le_mono Suc_pred diff_less less_numeral_extra(1) order_less_le_trans)
have len_1_tr: "length (drop ?k π) = 1"
using len_pi_geq1 by fastforce
have len_1: "length (drop (length π - 1) π) = 1"
using len_1_tr by blast
{assume * : "complen_mltl φ = 1"
then have "complen_mltl (formula_progression φ (take (length π - 1) π))
≤ 1" using assms complen_one_implies_one[of φ "take (length π - 1) π"]
by simp
} moreover {assume *: "complen_mltl (formula_progression φ (take (length π - 1) π))
≤ complen_mltl φ - length (take (length π - 1) π)"
then have "complen_mltl (formula_progression φ (take (length π - 1) π))
≤ 1"
using assms len_pi_geq1 by simp
} moreover {assume *: "complen_mltl (formula_progression φ (take (length π - 1) π)) = 1"
then have "complen_mltl (formula_progression φ (take (length π - 1) π))
≤ 1"
by simp
}
ultimately have "complen_mltl (formula_progression φ (take (length π - 1) π))
≤ 1"
using assms formula_progression_decreases_complen[of φ "(take (length π - 1) π)"]
by blast
then have "complen_mltl (formula_progression φ (take (length π - 1) π))
≤ length (drop (length π - 1) π)"
using len_1
by auto
then have t2: "(semantic_equiv (formula_progression (formula_progression φ (take ?k π)) (drop ?k π))
True_mltl) = semantics_mltl (drop ?k π) (formula_progression φ (take ?k π))"
using formula_progression_correctness_len1[of "drop ?k π" "(formula_progression φ (take ?k π ))"]
assms using len_1_tr
using formula_progression_well_definedness_preserved
by blast
have t3: "formula_progression (formula_progression φ (take ?k π)) (drop ?k π)
= formula_progression φ π "
using formula_progression_decomposition assms
by (metis "*" One_nat_def Suc_leI diff_le_self zero_less_diff)
have "length (take ?k π) > 0"
using *
by simp
then have ?thesis
using t1 t2 t3 by argo
}
ultimately show ?thesis
using assms len_pi_geq1
by linarith
qed
text ‹Adds the crucial assumption that the length of the trace
is greater than or equal to the computation length of the formula.›
corollary formula_progression_append:
fixes φ::"'a mltl"
assumes "intervals_welldef φ"
assumes "π ⊨⇩m φ"
assumes "length π ≥ complen_mltl φ"
shows "(π @ ζ) ⊨⇩m φ"
proof -
have len_geq1: "length π ≥ 1"
using assms(3) complen_geq_1 [of φ]
by auto
have h1: "semantic_equiv (formula_progression φ π) True_mltl"
using len_geq1 formula_progression_correctness assms
by blast
have take_length: "π = (take (length π) (π @ ζ ))"
by simp
have drop_length: "ζ = (drop (length π) (π @ ζ ))"
by simp
have "semantics_mltl ( ζ) True_mltl"
using semantics_mltl.simps(1) by auto
then show ?thesis
using len_geq1 h1 satisfiability_preservation[of "length π"]
take_length drop_length assms linorder_le_less_linear take_all
by (smt (verit, del_insts) semantic_equiv_def)
qed
paragraph ‹Converse of Corollary and Combined Statement›
text ‹Alternate statement of the formula progression correctness lemma
that asserts formula progression on a trace of length one is
semantically equivalent to False mltl when the formula is not satisfied›
lemma formula_progression_correctness_len1_helper_alt:
fixes φ::"'a mltl"
assumes "length π = 1"
assumes "intervals_welldef φ"
assumes "length π ≥ complen_mltl φ"
shows "((formula_progression_len1 φ (π ! 0)) ≡⇩m False⇩m) ⟷ ¬ ([π!0] ⊨⇩m φ)"
using assms
proof -
show ?thesis using assms
proof (induction φ)
case True_mltl
then show ?case
by (simp add: semantic_equiv_def)
next
case False_mltl
then show ?case by (simp add: semantic_equiv_def)
next
case (Prop_mltl x)
then show ?case
by (simp add: semantic_equiv_def)
next
case (Not_mltl φ)
then have "semantic_equiv (formula_progression_len1 φ (π ! 0)) False_mltl =
(¬ semantics_mltl [π ! 0] φ)"
by simp
then have "(∀ξ. semantics_mltl ξ (formula_progression_len1 φ (π ! 0)) =
False) = (¬ semantics_mltl [π ! 0] φ)"
unfolding semantic_equiv_def
by (meson semantics_mltl.simps(2))
then show ?case unfolding semantics_mltl.simps formula_progression_len1.simps
unfolding semantic_equiv_def
using complen_bounded_by_1
using Not_mltl.prems(2) Not_mltl.prems(3) assms(1) by auto
next
case (And_mltl φ1 φ2)
then show ?case
using formula_progression_len1.simps(5) semantic_equiv_def semantics_mltl.simps(1) semantics_mltl.simps(5)
intervals_welldef.simps(5) complen_bounded_by_1
by (smt (verit, ccfv_threshold) formula_progression_correctness_len1_helper semantics_mltl.simps(2))
next
case (Or_mltl φ1 φ2)
then have ind1: "semantic_equiv (formula_progression_len1 φ1 (π ! 0)) False_mltl = (¬ semantics_mltl [π ! 0] φ1)"
by simp
have ind2: "semantic_equiv (formula_progression_len1 φ2 (π ! 0)) False_mltl = (¬ semantics_mltl [π ! 0] φ2)"
using Or_mltl
by simp
show ?case
using complen_bounded_by_1 ind2 ind1
by (smt (verit) formula_progression_len1.simps(6) semantic_equiv_def semantics_mltl.simps(2) semantics_mltl.simps(6))
next
case (Future_mltl a b φ)
then show ?case
by (smt (verit, del_insts) Cons_nth_drop_Suc add.commute add_diff_cancel_right' complen_geq_one complen_mltl.simps(8) drop0 formula_progression_len1.simps(10) intervals_welldef.simps(7) leD le_add2 le_imp_less_Suc le_zero_eq list.size(4) nle_le plus_1_eq_Suc semantics_mltl.simps(7))
next
case (Global_mltl a b φ)
then show ?case using One_nat_def add_diff_cancel_left' add_diff_cancel_right' complen_geq_one complen_mltl.simps(7) drop0 formula_progression_len1.simps(10) formula_progression_len1.simps(4) formula_progression_len1.simps(9) impossible_Cons intervals_welldef.simps(8) le_add2 le_zero_eq less_numeral_extra(3) nle_le plus_1_eq_Suc semantic_equiv_def semantics_mltl.simps(4) semantics_mltl.simps(8)
by (smt (verit))
next
case (Until_mltl φ1 a b φ2)
have "max (complen_mltl φ1 - 1) (complen_mltl φ2) ≥ 1"
using complen_geq_1
using max.coboundedI2 by blast
then have "a = 0 ∧ b = 0"
using Until_mltl(4) complen_geq_1 unfolding complen_mltl.simps
by (metis Until_mltl.prems(3) add_diff_cancel_right' assms(1) bot_nat_0.extremum complen_mltl.simps(10) diff_is_0_eq' intervals_welldef.simps(9) le_antisym)
then show ?case
using complen_bounded_by_1
using Until_mltl.IH(2) Until_mltl.prems(2) Until_mltl.prems(3) assms(1) by force
next
case (Release_mltl φ1 a b φ2)
have ind2: " semantic_equiv (formula_progression_len1 φ2 (π ! 0)) False_mltl = (¬ semantics_mltl [π ! 0] φ2)"
using Release_mltl
by simp
have "max (complen_mltl φ1 - 1) (complen_mltl φ2) ≥ 1"
using complen_geq_1
using max.coboundedI2 by blast
then have "a = 0 ∧ b = 0"
using Release_mltl(4) complen_geq_1 unfolding complen_mltl.simps
by (metis Release_mltl.prems(3) add_diff_cancel_right' assms(1) bot_nat_0.extremum complen_mltl.simps(9) diff_is_0_eq' intervals_welldef.simps(10) le_antisym)
then have "formula_progression_len1 (Release_mltl φ1 a b φ2) (π ! 0) = Not_mltl ( Not_mltl (formula_progression_len1 φ2 (π ! 0)))"
unfolding formula_progression_len1.simps by auto
then show ?case using complen_bounded_by_1 ind2
by (smt (verit, ccfv_threshold) One_nat_def ‹a = 0 ∧ b = 0› add.commute diff_diff_cancel diff_is_0_eq' drop0 le_numeral_extra(3) list.size(3) list.size(4) not_not_equiv not_one_le_zero plus_1_eq_Suc semantic_equiv_def semantics_mltl.simps(10))
qed
qed
text ‹Alternate statement of the formula-progression-correctness lemma
with False in the case that the semantics are not satisfied.›
lemma formula_progression_correctness_len1_alt:
fixes φ::"'a mltl"
assumes "length π = 1"
assumes "intervals_welldef φ"
assumes "length π ≥ complen_mltl φ"
shows "((formula_progression φ π) ≡⇩m False_mltl) ⟷ ¬ π ⊨⇩m φ"
using assms formula_progression_correctness_len1_helper_alt
by (metis Cons_nth_drop_Suc One_nat_def drop0 drop_eq_Nil2 formula_progression.simps le_numeral_extra(4) zero_less_one zero_neq_one)
theorem formula_progression_correctness_alt:
fixes φ::"'a mltl"
assumes "intervals_welldef φ"
assumes "length π ≥ complen_mltl φ"
shows "((formula_progression φ π) ≡⇩m False_mltl) ⟷ ¬ (π ⊨⇩m φ)"
proof -
have len_pi_geq1: "length π ≥ 1"
using assms complen_geq_1[of φ]
by simp
{assume *: "length π = 1"
then have ?thesis using assms
using formula_progression_correctness_len1_alt assms by blast
} moreover {assume *: "length π > 1"
let ?k = "length π - 1"
have t1: "semantics_mltl (drop ?k π) (formula_progression φ (take ?k π ))
⟷ semantics_mltl π φ"
using satisfiability_preservation assms * len_pi_geq1
by (metis One_nat_def Suc_leI Suc_le_mono Suc_pred diff_less less_numeral_extra(1) order_less_le_trans)
have len_1_tr: "length (drop ?k π) = 1"
using len_pi_geq1 by fastforce
have len_1: "length (drop (length π - 1) π) = 1"
using len_1_tr by blast
{assume * : "complen_mltl φ = 1"
then have "complen_mltl (formula_progression φ (take (length π - 1) π))
≤ 1" using assms complen_one_implies_one[of φ "take (length π - 1) π"]
by simp
} moreover {assume *: "complen_mltl (formula_progression φ (take (length π - 1) π))
≤ complen_mltl φ - length (take (length π - 1) π)"
then have "complen_mltl (formula_progression φ (take (length π - 1) π))
≤ 1"
using assms len_pi_geq1 by simp
} moreover {assume *: "complen_mltl (formula_progression φ (take (length π - 1) π)) = 1"
then have "complen_mltl (formula_progression φ (take (length π - 1) π))
≤ 1"
by simp
}
ultimately have "complen_mltl (formula_progression φ (take (length π - 1) π))
≤ 1"
using assms formula_progression_decreases_complen[of φ "(take (length π - 1) π)"]
by blast
then have "complen_mltl (formula_progression φ (take (length π - 1) π))
≤ length (drop (length π - 1) π)"
using len_1
by auto
then have t2: "(semantic_equiv (formula_progression (formula_progression φ (take ?k π)) (drop ?k π))
True_mltl) = semantics_mltl (drop ?k π) (formula_progression φ (take ?k π))"
using formula_progression_correctness_len1[of "drop ?k π" "(formula_progression φ (take ?k π ))"]
assms using len_1_tr
using formula_progression_well_definedness_preserved
by blast
have t3: "formula_progression (formula_progression φ (take ?k π)) (drop ?k π)
= formula_progression φ π "
using formula_progression_decomposition assms
by (metis "*" One_nat_def Suc_leI diff_le_self zero_less_diff)
have "length (take ?k π) > 0"
using *
by simp
then have ?thesis
using t1 t2 t3
by (metis ‹complen_mltl (formula_progression φ (take (length π - 1) π)) ≤ length (drop (length π - 1) π)› assms(1) formula_progression_correctness_len1_alt formula_progression_well_definedness_preserved len_1_tr)
}
ultimately show ?thesis
using assms len_pi_geq1
by linarith
qed
lemma formula_progression_true_or_false:
fixes φ::"'a mltl"
assumes "intervals_welldef φ"
assumes "length π ≥ complen_mltl φ"
shows "((formula_progression φ π) ≡⇩m False⇩m) ∨
((formula_progression φ π) ≡⇩m True⇩m)"
using formula_progression_correctness formula_progression_correctness_alt
using assms by blast
text ‹The inverse statement of formula-progression-append lemma›
corollary formula_progression_append_converse:
fixes φ::"'a mltl"
assumes "intervals_welldef φ"
assumes "¬ π ⊨⇩m φ"
assumes "length π ≥ complen_mltl φ"
shows "¬ (π @ ζ) ⊨⇩m φ"
proof-
have len_geq1: "length π ≥ 1"
using assms(3) complen_geq_1 [of φ]
by auto
have h1: "semantic_equiv (formula_progression φ π) False_mltl"
using len_geq1 formula_progression_correctness_alt assms by blast
have take_length: "π = (take (length π) (π @ ζ ))"
by simp
have drop_length: "ζ = (drop (length π) (π @ ζ ))"
by simp
have "semantics_mltl ( ζ) True_mltl"
using semantics_mltl.simps(1) by auto
then show ?thesis
using len_geq1 h1 satisfiability_preservation[of "length π"]
take_length drop_length assms linorder_le_less_linear take_all
by (smt (verit) semantic_equiv_def semantics_mltl.simps(2))
qed
text ‹An important property of complen-mltl that says states in the trace
after the computation length does not affect the semantic
satisfaction of the formula.›
corollary complen_property:
fixes φ::"'a mltl"
assumes "intervals_welldef φ"
assumes "length π ≥ complen_mltl φ"
shows "π ⊨⇩m φ ⟷ (∀ζ. (π @ ζ) ⊨⇩m φ)"
using formula_progression_append
using formula_progression_append_converse assms by blast
subsection "Formula Progression Examples"
value "formula_progression
((G⇩m [0,2] (Prop_mltl 0))::nat mltl)
[{0::nat}, {0}, {1}]"
value "[{0::nat}, {0}, {1}] ! 0"
value "drop 1 ([{0::nat}, {0}, {1}])"
value "formula_progression_len1 ((G⇩m [0,2] (Prop_mltl 0))::nat mltl) {0}"
value "formula_progression
(formula_progression_len1
((G⇩m [0,2] (Prop_mltl 0))::nat mltl)
{0}
)
[{0}, {1}]"
value "formula_progression
((G⇩m [0,1] (Prop_mltl 0))::nat mltl)
[{0}, {1}]"
value "formula_progression
(formula_progression_len1
((Global_mltl 0 1 (Prop_mltl 0))::nat mltl)
{0})
[{1}]"
value "formula_progression_len1 ((G⇩m [0,1] (Prop_mltl 0))::nat mltl) {0}"
value "formula_progression
((G⇩m [0,0] (Prop_mltl 0))::nat mltl)
[{1}]"
value "formula_progression_len1
((G⇩m [0,0] (Prop_mltl 0))::nat mltl)
{1}"
subsection ‹Code Export›
export_code
formula_progression
in SML module_name FP
end