Theory LTL3
theory LTL3
imports Main Traces AnswerIndexedFamilies LinearTemporalLogic
begin
chapter ‹LTL3: Semantics, Equivalence and Formula Progression›
type_synonym 'a AiF⇩3 = ‹answer ⇒ 'a state dset›
primrec and_AiF⇩3 :: ‹'a AiF⇩3 ⇒ 'a AiF⇩3 ⇒ 'a AiF⇩3› (infixl ‹∧⇩3·› 60) where
‹(a ∧⇩3· b) T = a T ⊓ b T›
| ‹(a ∧⇩3· b) F = a F ⊔ b F›
primrec or_AiF⇩3 :: ‹'a AiF⇩3 ⇒ 'a AiF⇩3 ⇒ 'a AiF⇩3› (infixl ‹∨⇩3·› 59) where
‹(a ∨⇩3· b) T = a T ⊔ b T›
| ‹(a ∨⇩3· b) F = a F ⊓ b F›
fun not_AiF⇩3 :: ‹'a AiF⇩3 ⇒ 'a AiF⇩3› (‹¬⇩3· _›) where
‹(¬⇩3· a) T = a F›
| ‹(¬⇩3· a) F = a T›
fun univ_AiF⇩3 :: ‹'a AiF⇩3› (‹T⇩3∙›) where
‹T⇩3∙ T = Σ∞›
| ‹T⇩3∙ F = ∅›
fun lsatisfying_AiF⇩3 :: ‹'a ⇒ 'a AiF⇩3› (‹lsat⇩3∙›) where
‹lsat⇩3∙ x T = compr (λt. t ≠ ε ∧ x ∈ L (thead t))›
| ‹lsat⇩3∙ x F = compr (λt. t ≠ ε ∧ x ∉ L (thead t))›
fun x⇩3_operator :: ‹'a AiF⇩3 ⇒ 'a AiF⇩3› (‹X⇩3·›) where
‹X⇩3· t T = prepend (t T)›
| ‹X⇩3· t F = prepend (t F)›
fun iterate :: ‹('a ⇒ 'a) ⇒ nat ⇒ ('a ⇒ 'a)› where
‹iterate f 0 x = x›|
‹iterate f (Suc n) x = f (iterate f n x)›
primrec u⇩3_operator :: ‹'a AiF⇩3 ⇒ 'a AiF⇩3 ⇒ 'a AiF⇩3› (infix ‹U⇩3·› 61) where
‹(a U⇩3· b) T = ⨆ ( range (λi. iterate (λx. prepend x ⊓ a T) i (b T) ))›
| ‹(a U⇩3· b) F = ⨅ ( range (λi. iterate (λx. prepend x ⊔ a F) i (b F) ))›
fun triv_true :: ‹'a ⇒ bool› where
‹triv_true x = (∀s. x∈ L s)›
fun triv_false :: ‹'a ⇒ bool› where
‹triv_false x = (∀s. x∉ L s)›
fun nontrivial :: ‹'a ⇒ bool› where
‹nontrivial x = ((∃s. x∈ L s) ∧ (∃t. x∉ L t))›
fun zero_length :: ‹'a trace ⇒ bool› where
‹zero_length (Finite t) = (length t = 0)›
| ‹zero_length (Infinite t) = False›
fun ltl_semantics⇩3 :: ‹'a ltl ⇒ 'a AiF⇩3› (‹⟦_⟧⇩3›) where
‹⟦ true⇩l ⟧⇩3 = T⇩3∙›
| ‹⟦ not⇩l φ ⟧⇩3 = ¬⇩3· ⟦φ⟧⇩3›
| ‹⟦ prop⇩l(a) ⟧⇩3 = lsat⇩3∙ a›
| ‹⟦ φ or⇩l ψ ⟧⇩3 = ⟦φ⟧⇩3 ∨⇩3· ⟦ψ⟧⇩3›
| ‹⟦ φ and⇩l ψ ⟧⇩3 = ⟦φ⟧⇩3 ∧⇩3· ⟦ψ⟧⇩3›
| ‹⟦ X⇩l φ ⟧⇩3 = X⇩3· ⟦φ⟧⇩3›
| ‹⟦ φ U⇩l ψ ⟧⇩3 = ⟦φ⟧⇩3 U⇩3· ⟦ψ⟧⇩3›
section ‹LTL/LTL3 equivalence›
declare dset.Inf_insert[simp del]
declare dset.Sup_insert[simp del]
lemma itdrop_all_split:
assumes ‹x ∈ A› and ‹∀i<k. itdrop (Suc i) x ∈ A›
shows ‹i < Suc k ⟹ itdrop i x ∈ A›
using assms proof (cases ‹i›)
qed (auto simp: itdrop_def)
lemma itdrop_exists_split[simp]:
shows ‹(∃i<Suc k. itdrop i x ∈ A) ⟷ (∃i < k. itdrop (Suc i) x ∈ A) ∨ x ∈ A›
proof (rule iffI)
{ fix i
assume ‹i < Suc k› ‹itdrop i x ∈ A› ‹x ∉ A›
then have ‹∃i<k. itdrop (Suc i) x ∈ A›
proof (cases ‹i›)
qed auto
} then show ‹ ∃i<Suc k. itdrop i x ∈ A ⟹ (∃i<k. itdrop (Suc i) x ∈ A) ∨ x ∈ A› by auto
next
assume ‹(∃i<k. itdrop (Suc i) x ∈ A) ∨ x ∈ A›
then show ‹∃i<Suc k. itdrop i x ∈ A›
by auto
qed
lemma until_iterate :
‹{x. ∃k. (∀i<k. itdrop i x ∈ A) ∧ itdrop k x ∈ B} = ⋃ (range (λk. iterate (λx. iprepend x ∩ A) k B))›
proof (rule set_eqI; rule iffI)
fix x
{ fix k
assume ‹∀i<k. itdrop i x ∈ A › and ‹itdrop k x ∈ B›
then have ‹x ∈ iterate (λx. iprepend x ∩ A) k B›
proof (induct ‹k› arbitrary: ‹x›)
case 0
then show ‹?case› by simp
next
case (Suc k)
from this(2,3) show ‹?case›
by (auto intro!: Suc.hyps[where x = ‹itdrop 1 x›, simplified])
qed }
then show ‹x ∈ {x. ∃k. (∀i<k. itdrop i x ∈ A) ∧ itdrop k x ∈ B}
⟹ x ∈ (⋃k. iterate (λx. iprepend x ∩ A) k B)›
by blast
next
fix x
{ fix k
assume ‹x ∈ iterate (λx. iprepend x ∩ A) k B›
then have ‹(∀i<k. itdrop i x ∈ A) ∧ itdrop k x ∈ B ›
proof (induct ‹k› arbitrary: ‹x›)
case 0
then show ‹?case› by auto
next
case (Suc k)
from this(2) show ‹?case›
by (auto dest: Suc.hyps[where x = ‹itdrop 1 x›, simplified]
intro: itdrop_all_split)
qed }
then show ‹x ∈ (⋃k. iterate (λx. iprepend x ∩ A) k B) ⟹ x ∈ {x. ∃k. (∀i<k. itdrop i x ∈ A) ∧ itdrop k x ∈ B}›
by blast
qed
lemma release_iterate:
‹ {u. ∀k. (∃i<k. itdrop i u ∈ A) ∨ itdrop k u ∈ B} = ⋂ (range (λi. iterate (λx. iprepend x ∪ A) i B))›
proof (rule set_eqI; rule iffI)
fix x
{ fix i assume ‹ ∀k. (∃i<k. itdrop i x ∈ A) ∨ itdrop k x ∈ B›
then have ‹x ∈ iterate (λx. iprepend x ∪ A) i B›
proof (induct ‹i› arbitrary: ‹x›)
case 0
then show ‹?case› by auto
next
case (Suc i)
show ‹?case›
apply (clarsimp)
apply (rule Suc.hyps[where x = ‹itdrop 1 x›, simplified])
using Suc(2)[THEN spec, where x = ‹Suc _›,simplified]
by auto
qed }
then show ‹x ∈ {u. ∀k. (∃i<k. itdrop i u ∈ A) ∨ itdrop k u ∈ B} ⟹ x ∈ (⋂i. iterate (λx. iprepend x ∪ A) i B)›
by auto
next
fix x
{ fix k
assume ‹ ∀i. x ∈ iterate (λx. iprepend x ∪ A) i B›
then have P: ‹∀i. x ∈ iterate (λx. iprepend x ∪ A) i B›
by blast
assume ‹itdrop k x ∉ B› with P have ‹∃i<k. itdrop i x ∈ A›
proof (induct ‹k› arbitrary: ‹x›)
case 0
then show ‹?case› by (simp, metis iterate.simps(1))
next
case (Suc k)
from this(3) show ‹?case›
apply clarsimp
apply (rule Suc.hyps[where x = ‹itdrop 1 x›, simplified])
using Suc(2)[THEN spec, where x = ‹Suc _›]
by auto
qed }
then show ‹x ∈ (⋂i. iterate (λx. iprepend x ∪ A) i B) ⟹ x ∈ {u. ∀k. (∃i<k. itdrop i u ∈ A) ∨ itdrop k u ∈ B}›
by auto
qed
lemma property_until_iterate:
‹property (iterate (λx. prepend x ⊓ A) k B) = iterate (λx. iprepend x ∩ property A) k (property B)›
by (induct ‹k›, auto simp: property_Inter property_prepend)
lemma property_release_iterate:
‹property (iterate (λx. prepend x ⊔ A) k B) = iterate (λx. iprepend x ∪ property A) k (property B)›
by (induct ‹k›, auto simp: property_Union property_prepend)
lemma ltl3_equiv_ltl:
shows ‹property (⟦ φ ⟧⇩3 T) = ⟦ φ ⟧⇩l T›
and ‹property (⟦ φ ⟧⇩3 F) = ⟦ φ ⟧⇩l F›
proof (induct ‹φ›)
case True_ltl
{
case 1
then show ‹?case› by (simp, transfer, simp)
next
case 2
then show ‹?case› by (simp, transfer, simp)
}
next
case (Not_ltl φ)
{
case 1
then show ‹?case› using Not_ltl by simp
next
case 2
then show ‹?case› using Not_ltl by simp
}
next
case (Prop_ltl x)
{
case 1
then show ‹?case›
apply simp
apply transfer
apply (simp add: infinites_dprefixes)
apply (clarsimp simp add: infinites_def split: trace.split_asm trace.split)
apply (rule set_eqI, rule iffI)
apply (clarsimp split: trace.split_asm trace.split)
apply (metis zero_length.cases)
apply (clarsimp split: trace.split_asm trace.split)
by (metis Traces.append.simps(3) append_is_empty(2) trace.distinct(1) trace.inject(2))
next
case 2
then show ‹?case›
apply simp
apply transfer
apply (simp add: infinites_dprefixes)
apply (clarsimp simp add: infinites_def split: trace.split_asm trace.split)
apply (rule set_eqI, rule iffI)
apply (clarsimp split: trace.split_asm trace.split)
apply (metis zero_length.cases)
apply (clarsimp split: trace.split_asm trace.split)
by (metis Traces.append.simps(3) append_is_empty(2) trace.distinct(1) trace.inject(2))
}
next
case (Or_ltl φ1 φ2)
{
case 1
then show ‹?case› by (simp add: property_Union Or_ltl)
next
case 2
then show ‹?case› by (simp add: property_Inter Or_ltl)
}
next
case (And_ltl φ1 φ2)
{
case 1
then show ‹?case› by (simp add: property_Inter And_ltl)
next
case 2
then show ‹?case› by (simp add: property_Union And_ltl)
}
next
case (Next_ltl φ)
{
case 1
then show ‹?case› by (simp add: property_prepend Next_ltl iprepend_def)
next
case 2
then show ‹?case› by (simp add: property_prepend Next_ltl iprepend_def)
}
next
case (Until_ltl φ1 φ2)
{
case 1
then show ‹?case›
apply (simp add: Until_ltl[THEN sym] property_Union image_Collect property_until_iterate)
using until_iterate[simplified] by blast
next
case 2
then show ‹?case›
apply (simp add: Until_ltl[THEN sym] property_Inter image_Collect property_release_iterate)
using release_iterate[simplified] by metis
}
qed
section ‹Equivalence to LTL3 of Bauer et al.›
lemma extension_lemma: ‹in_dset t A = (∀ω. t ⌢ Infinite ω ∈ Infinite ` property A)›
proof transfer
fix t and A :: ‹'a trace set›
assume D: ‹definitive A›
show ‹t ∈ A = (∀ω. t ⌢ Infinite ω ∈ Infinite ` infinites A) ›
proof (rule iffI)
assume ‹t ∈ A›
with D have D': ‹↑ t ⊆ A › by (rule definitive_contains_extensions)
{ fix ω have ‹t ⌢ Infinite ω ∈ A›
by (rule subsetD[OF D'], force simp add: extensions_def)
} then have ‹ ∀ω. t ⌢ Infinite ω ∈ A› by auto
thus ‹ ∀ω. t ⌢ Infinite ω ∈ Infinite ` infinites A›
by (simp add: infinites_append_right infinites_alt)
next
assume ‹ ∀ω. t ⌢ Infinite ω ∈ Infinite ` infinites A› then
have inA: ‹ ∀ω. t ⌢ Infinite ω ∈ A›
by (simp add: infinites_alt infinites_append_right)
have ‹↑ t ⊆ ↓⇩s A›
proof -
{ fix u
obtain ω :: ‹'a infinite_trace› where ‹Infinite ω = u ⌢ Infinite undefined›
by (cases ‹u›; simp)
then have ‹∃v. (t ⌢ u) ⌢ v ∈ A›
using inA[THEN spec, where x = ‹ω›] by (metis trace.assoc)
} thus ‹?thesis› unfolding extensions_def prefix_closure_def prefixes_def by auto
qed
with D show ‹t ∈ A› by (rule definitive_elemI)
qed
qed
lemma extension:
shows ‹in_dset t (ltl_semantics⇩3 φ T) = (∀ω. (t ⌢ Infinite ω) ∈ Infinite ` (ltl_semantics φ T))›
and ‹in_dset t (ltl_semantics⇩3 φ F) = (∀ω. (t ⌢ Infinite ω) ∈ Infinite ` (ltl_semantics φ F))›
by (simp_all add: ltl3_equiv_ltl[THEN sym] extension_lemma)
section ‹Formula Progression›
fun progress :: ‹'a ltl ⇒ 'a state ⇒ 'a ltl› where
‹progress true⇩l σ = true⇩l›
| ‹progress (not⇩l φ) σ = not⇩l (progress φ) σ›
| ‹progress (prop⇩l(a)) σ = (if a ∈ L σ then true⇩l else not⇩l true⇩l)›
| ‹progress (φ or⇩l ψ) σ = (progress φ σ) or⇩l (progress ψ σ)›
| ‹progress (φ and⇩l ψ) σ = (progress φ σ) and⇩l (progress ψ σ)›
| ‹progress (X⇩l φ) σ = φ›
| ‹progress (φ U⇩l ψ) σ = (progress ψ σ) or⇩l ((progress φ σ) and⇩l (φ U⇩l ψ))›
lemma unroll_Union: ‹⨆ (range P) = P 0 ⊔ (⨆ (range (P ∘ Suc)))›
apply (rule definitives_inverse_eqI)
apply (simp add: property_Union)
apply (rule dset.order_antisym)
apply (clarsimp intro!: definitives_mono; metis not0_implies_Suc)
by (force intro: definitives_mono)
lemma unroll_Inter: ‹⨅ (range P) = P 0 ⊓ (⨅ (range (P ∘ Suc)))›
apply (rule definitives_inverse_eqI)
apply (simp add: property_Inter)
apply (rule dset.order_antisym)
apply (force intro: definitives_mono)
by (clarsimp intro!: definitives_mono; metis not0_implies_Suc)
lemma iterates_nonempty: ‹range (λi. iterate f i X) ≠ {}›
by blast
lemma until_cont: ‹A ≠ {} ⟹ prepend (⨆ A) ⊓ X = ⨆ ((λx. prepend x ⊓ X) ` A)›
by (simp add: prepend_Union[THEN sym] dset.SUP_inf)
lemma release_cont: ‹A ≠ {} ⟹ prepend (⨅ A) ⊔ X = ⨅ ((λx. prepend x ⊔ X) ` A)›
by (simp add: prepend_Inter[THEN sym] dset.INF_sup)
lemma iterate_unroll_Inter:
assumes ‹⋀A. A ≠ {} ⟹ f (⨅ A) = ⨅ (f ` A)›
shows ‹⨅ (range (λi. iterate f i X)) = X ⊓ f (⨅ (range (λi. iterate f i X )))›
apply (subst unroll_Inter)
by (force simp: assms[OF iterates_nonempty] property_Inter intro: definitives_inverse_eqI)
lemma iterate_unroll_Union:
assumes ‹⋀A. A ≠ {} ⟹ f (⨆ A) = ⨆ (f ` A)›
shows ‹⨆ (range (λi. iterate f i X)) = X ⊔ f (⨆ (range (λi. iterate f i X )))›
apply (subst unroll_Union)
by (force simp: assms[OF iterates_nonempty] property_Union intro: definitives_inverse_eqI)
lemma inf_inf: ‹x ⊓ (y ⊓ z) = (x ⊓ y) ⊓ (x ⊓ z)›
by (simp add: dset.inf_assoc dset.inf_left_commute)
theorem progression_tf :
‹prepend (⟦progress φ σ ⟧⇩3 T) ⊓ compr (λt. t ≠ ε ∧ thead t = σ) ⊑ ⟦ φ ⟧⇩3 T ›
‹prepend (⟦progress φ σ ⟧⇩3 F) ⊓ compr (λt. t ≠ ε ∧ thead t = σ) ⊑ ⟦ φ ⟧⇩3 F ›
proof (induct ‹φ›)
case True_ltl
{
case 1
then show ‹?case› by simp
next
case 2
then show ‹?case› by (simp, transfer, simp add: prepend'_def)
}
next
case (Not_ltl φ)
{
case 1
then show ‹?case› using Not_ltl by simp
next
case 2
then show ‹?case› using Not_ltl by simp
}
next
case (Prop_ltl x)
{
case 1
then show ‹?case›
by (simp, transfer, auto simp: prepend'_def intro: dprefixes_mono[THEN subsetD, rotated])
next
case 2
then show ‹?case›
by (simp, transfer, auto simp: prepend'_def intro: dprefixes_mono[THEN subsetD, rotated])
}
next
case (Or_ltl φ1 φ2)
{
case 1
then show ‹?case›
apply (simp add: prepend_Union[THEN sym])
using Or_ltl(1, 3)
by (metis (no_types, lifting) dset.inf_sup_distrib2 dset.sup_mono)
next
case 2
then show ‹?case›
apply (simp add: prepend_Inter[THEN sym])
using Or_ltl(2,4)
by (meson dset.dual_order.refl dset.dual_order.trans dset.inf.coboundedI2
dset.inf_le1 dset.inf_mono)
}
next
case (And_ltl φ1 φ2)
{
case 1
then show ‹?case›
apply (simp add: prepend_Inter[THEN sym])
using And_ltl(1,3)
by (meson dset.dual_order.trans dset.inf_le1 dset.inf_le2 dset.le_infI)
next
case 2
then show ‹?case›
apply (simp add: prepend_Union[THEN sym])
using And_ltl(2, 4)
by (metis (no_types, lifting) dset.inf_sup_distrib2 dset.sup_mono)
}
next
case (Next_ltl φ)
{
case 1
then show ‹?case› by simp
next
case 2
then show ‹?case› by simp
}
next
case (Until_ltl φ1 φ2)
{
case 1
then show ‹?case›
apply (simp only: progress.simps)
apply (simp add: prepend_Union[THEN sym] prepend_Inter[THEN sym])
apply (subst dset.inf_commute)
apply (subst dset.distrib(3))
apply (rule dset.order_trans)
apply (rule dset.sup_mono[OF _ dset.order_refl])
apply (subst dset.inf_commute)
apply (rule Until_ltl(3))
apply (subst dset.inf_assoc[THEN sym])
apply (rule dset.order_trans)
apply (rule dset.sup_mono[OF dset.order_refl])
apply (rule dset.inf_mono[OF _ dset.order_refl])
apply (subst dset.inf_commute)
apply (rule Until_ltl(1))
apply (subst iterate_unroll_Union[OF until_cont], simp)
by (simp add: dset.inf.commute prepend_Union)
next
case 2
then show ‹?case›
apply simp
apply (subst prepend_Inter[THEN sym] prepend_Union[THEN sym], simp)
apply (subst dset.inf_commute)
apply (subst inf_inf)
apply (rule dset.order_trans)
apply (rule dset.inf_mono)
apply (subst dset.inf_commute)
apply (rule Until_ltl(4))
apply (simp add: prepend_Union[THEN sym])
apply (subst dset.distrib(3))
apply (rule dset.sup_mono)
apply (subst dset.inf_commute)
apply (rule Until_ltl(2))
apply (rule dset.le_infI2, rule dset.order_refl)
apply (subst iterate_unroll_Inter[OF release_cont,simplified]; simp)
by (metis dset.inf_le2 dset.sup.commute)
}
qed
theorem progression_tf' :
‹⟦ φ ⟧⇩3 T ⊓ compr (λt. t ≠ ε ∧ thead t = σ) ⊑ prepend (⟦progress φ σ ⟧⇩3 T) ›
‹⟦ φ ⟧⇩3 F ⊓ compr (λt. t ≠ ε ∧ thead t = σ) ⊑ prepend (⟦progress φ σ ⟧⇩3 F) ›
proof (induct ‹φ›)
case True_ltl
{
case 1
then show ‹?case› by (simp, transfer, simp add: prepend'_def)
next
case 2
then show ‹?case› by simp
}
next
case (Not_ltl φ)
{
case 1
then show ‹?case› using Not_ltl by simp
next
case 2
then show ‹?case› using Not_ltl by simp
}
next
case (Prop_ltl x)
{
case 1
then show ‹?case› apply simp
apply transfer
apply clarsimp
apply (clarsimp simp: prepend'_def)
apply (subst compr'_inter_thead)
by (metis (mono_tags, lifting) Collect_empty_eq dprefixes_empty)
next
case 2
then show ‹?case›
apply simp
apply transfer
apply (clarsimp simp: prepend'_def)
apply (subst compr'_inter_thead)
by (metis (mono_tags, lifting) Collect_empty_eq dprefixes_empty)
}
next
case (Or_ltl φ1 φ2)
{
case 1
then show ‹?case›
apply (simp add: prepend_Union[THEN sym])
using Or_ltl(1,3)
by (metis (no_types, lifting) dset.inf_sup_distrib2 dset.sup_mono)
next
case 2
then show ‹?case›
apply (simp add: prepend_Inter[THEN sym])
using Or_ltl(2,4)
by (meson dset.dual_order.refl dset.dual_order.trans dset.inf.coboundedI2 dset.inf_le1 dset.inf_mono)
}
next
case (And_ltl φ1 φ2)
{
case 1
then show ‹?case›
apply (simp add: prepend_Inter[THEN sym])
using And_ltl(1,3)
by (meson dset.dual_order.refl dset.dual_order.trans dset.le_inf_iff)
next
case 2
then show ‹?case›
apply (simp add: prepend_Union[THEN sym])
using And_ltl(2,4)
by (metis (no_types,lifting) dset.inf_sup_distrib2 dset.sup_mono)
}
next
case (Next_ltl φ)
{
case 1
then show ‹?case› using Next_ltl by simp
next
case 2
then show ‹?case› using Next_ltl by simp
}
next
case (Until_ltl φ1 φ2)
{
case 1
then show ‹?case›
unfolding ltl_semantics⇩3.simps u⇩3_operator.simps
ltl_semantics.simps progress.simps u_operator.simps or_AiF⇩3.simps and_AiF⇩3.simps
apply (simp add: full_SetCompr_eq prepend_Union[THEN sym])
apply (rule dset.order_trans[rotated])
apply (rule dset.sup_mono [OF _ dset.order_refl], rule Until_ltl(3))
apply (simp add: prepend_Inter[THEN sym])
apply (rule dset.order_trans[rotated])
apply (rule dset.sup_mono [OF dset.order_refl])
apply (rule dset.inf_mono [OF _ dset.order_refl])
apply (rule Until_ltl(1))
apply (subst iterate_unroll_Union[OF until_cont], simp)
apply (subst dset.inf_commute)
apply (subst dset.inf_sup_distrib1)
apply (simp, rule conjI)
apply (subst dset.inf_commute)
apply auto[1]
by (meson dset.eq_refl dset.inf.boundedI dset.le_infE dset.le_supI2)
next
case 2
then show ‹?case›
unfolding ltl_semantics⇩3.simps u⇩3_operator.simps
ltl_semantics.simps progress.simps u_operator.simps or_AiF⇩3.simps and_AiF⇩3.simps
apply (simp add: full_SetCompr_eq prepend_Inter[THEN sym])
apply (rule conjI,rule dset.order_trans[rotated])
apply (rule Until_ltl(4))
apply (rule dset.inf_mono; simp?)
apply (metis iterate.simps(1) dset.Inf_lower rangeI)
apply (simp add: prepend_Union[THEN sym])
apply (rule dset.order_trans[rotated])
apply (rule dset.sup_mono)
apply (rule Until_ltl(2))
apply (rule dset.order_refl)
apply (subst iterate_unroll_Inter[OF release_cont], simp)
apply (simp add: prepend_Inter[THEN sym] image_image)
apply (subst dset.inf_assoc)
apply (subst dset.sup_inf_distrib2)
apply (rule dset.le_infI2)
by (simp add: dset.inf.coboundedI1 insert_commute)
}
qed
theorem progression_tf'_u:
shows ‹⟦ φ ⟧⇩3 A ⊓ compr (λt. t ≠ ε ∧ thead t = σ) ⊑ prepend (⟦progress φ σ ⟧⇩3 A)›
by (cases ‹A›; simp add: progression_tf')
theorem progression_tf_u:
shows ‹prepend (⟦progress φ σ ⟧⇩3 A) ⊓ compr (λt. t ≠ ε ∧ thead t = σ) ⊑ ⟦ φ ⟧⇩3 A›
by (cases ‹A›; simp add: progression_tf)
lemma fp_compr_helper: ‹in_dset (Finite (a # t)) (compr (λ x. x ≠ ε ∧ thead x = a))›
apply transfer
apply (simp add: dprefixes_def subset_iff extensions_def prefix_closure_def prefixes_def)
by (metis ε_def list.distinct(1) nth_Cons_0 thead.simps(1) thead_append trace.inject(1)
trace.left_neutral trace.right_neutral)
theorem fp:
shows ‹in_dset (Finite t) (⟦ φ ⟧⇩3 A) ⟷ ⟦ foldl progress φ t ⟧⇩3 A = Σ∞ ›
proof (induct ‹t› arbitrary: ‹φ›)
case Nil
then show ‹?case›
by (rule iffI; simp add: in_dset_ε[simplified ε_def] in_dset_UNIV)
next
case (Cons a t)
show ‹?case›
proof (simp add: Cons[where φ=‹progress φ a›, THEN sym], rule)
assume ‹in_dset (Finite (a # t)) (⟦φ⟧⇩3 A)›
then show ‹in_dset (Finite t) (⟦progress φ a⟧⇩3 A)›
by (force intro: in_dset_prependD in_dset_subset[OF progression_tf'_u]
in_dset_inter fp_compr_helper)
next
assume ‹in_dset (Finite t) (⟦progress φ a⟧⇩3 A)›
then show ‹in_dset (Finite (a # t)) (⟦φ⟧⇩3 A)›
by (force intro: in_dset_subset[OF progression_tf_u] in_dset_inter fp_compr_helper
in_dset_prependI[where x = ‹Finite u› for u, simplified])
qed
qed
lemma em_ltl: ‹⟦ φ ⟧⇩l T = UNIV - (⟦ φ ⟧⇩l F)›
by (rule set_eqI; clarsimp simp add: subset_iff ltl_equivalence[THEN sym])
theorem em:
shows ‹⟦ φ ⟧⇩3 T = complement (⟦ φ ⟧⇩3 F)›
by (force intro: definitives_inverse_eqI simp: ltl3_equiv_ltl em_ltl)
end