theory LTL3
  imports Main Traces AnswerIndexedFamilies LinearTemporalLogic
begin

chapter ‹LTL3: Semantics, Equivalence and Formula Progression›

type_synonym 'a AiF₃ = ‹answer → 'a state dset›

primrec and_AiF₃ :: ‹'a AiF₃ → 'a AiF₃ → 'a AiF₃› (infixl ‹∧₃⏹› 60) where
  ‹(a ∧₃⏹ b) T = a T ⊓ b T›
| ‹(a ∧₃⏹ b) F = a F ⊔ b F›

primrec or_AiF₃ :: ‹'a AiF₃ → 'a AiF₃ → 'a AiF₃› (infixl ‹∨₃⏹› 59) where
  ‹(a ∨₃⏹ b) T = a T ⊔ b T›
| ‹(a ∨₃⏹ b) F = a F ⊓ b F›

fun not_AiF₃ :: ‹'a AiF₃ → 'a AiF₃› (‹¬₃⏹ _›) where
  ‹(¬₃⏹ a) T = a F›
| ‹(¬₃⏹ a) F = a T›

fun univ_AiF₃ :: ‹'a AiF₃› (‹T₃∙›) where
  ‹T₃∙ T = Σ∞›
| ‹T₃∙ F = ∅›

fun lsatisfying_AiF₃ :: ‹'a → 'a AiF₃› (‹lsat₃∙›) where
  ‹lsat₃∙ x T = compr (λt. t ≠ ε ∧ x ∈ L (thead t))›
| ‹lsat₃∙ x F = compr (λt. t ≠ ε ∧ x ∉ L (thead t))›

fun x₃_operator :: ‹'a AiF₃ → 'a AiF₃› (‹X₃⏹›) where
  ‹X₃⏹ t T = prepend (t T)›
| ‹X₃⏹ 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₃_operator :: ‹'a AiF₃ → 'a AiF₃ → 'a AiF₃› (infix ‹U₃⏹› 61) where
  ‹(a U₃⏹ b) T = ⊔ ( range (λi. iterate (λx. prepend x ⊓ a T) i (b T) ))›
| ‹(a U₃⏹ 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₃ :: ‹'a ltl → 'a AiF₃› (‹[_]₃›) where
  ‹[ true_l ]₃ = T₃∙›
| ‹[ not_l φ ]₃ = ¬₃⏹ [φ]₃›
| ‹[ prop_l(a) ]₃ = lsat₃∙ a›
| ‹[ φ or_l ψ ]₃ = [φ]₃ ∨₃⏹ [ψ]₃›
| ‹[ φ and_l ψ ]₃ = [φ]₃ ∧₃⏹ [ψ]₃›
| ‹[ X_l φ ]₃ = X₃⏹ [φ]₃›
| ‹[ φ U_l ψ ]₃ = [φ]₃ U₃⏹ [ψ]₃›

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 ([ φ ]₃ T) = [ φ ]_l T›
  and   ‹property ([ φ ]₃ 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₃ φ T) = (∀ψ. (t ⌢ Infinite ψ) ∈ Infinite ` (ltl_semantics φ T))›
  and   ‹in_dset t (ltl_semantics<sub>3</sub> φ 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 φ σ ]₃ T) ⊓ compr (λt. t ≠ ε ∧ thead t = σ) ⊑ [ φ ]₃ T ›
  ‹prepend ([progress φ σ ]₃ F) ⊓ compr (λt. t ≠ ε ∧ thead t = σ) ⊑ [ φ ]₃ 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› (* TODO tidy*)
      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' :
  ‹[ φ ]₃ T ⊓ compr (λt. t ≠ ε ∧ thead t = σ) ⊑ prepend ([progress φ σ ]₃ T) ›
  ‹[ φ ]₃ F ⊓ compr (λt. t ≠ ε ∧ thead t = σ) ⊑ prepend ([progress φ σ ]₃ 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₃.simps u₃_operator.simps
              ltl_semantics.simps progress.simps u_operator.simps or_AiF₃.simps and_AiF₃.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₃.simps u₃_operator.simps
              ltl_semantics.simps progress.simps u_operator.simps or_AiF₃.simps and_AiF₃.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 ‹[ φ ]₃ A ⊓ compr (λt. t ≠ ε ∧ thead t = σ) ⊑ prepend ([progress φ σ ]₃ A)›
  by (cases ‹A›; simp add: progression_tf')

theorem progression_tf_u:
  shows ‹prepend ([progress φ σ ]₃ A) ⊓ compr (λt. t ≠ ε ∧ thead t = σ) ⊑ [ φ ]₃ 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) ([ φ ]₃ A) ⟷ [ foldl progress φ t ]₃ 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)) ([φ]₃ A)›
    then show ‹in_dset (Finite t) ([progress φ a]₃ 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]₃ A)›
    then show ‹in_dset (Finite (a # t)) ([φ]₃ 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 ‹[ φ ]₃ T = complement ([ φ ]₃ F)›
  by (force intro: definitives_inverse_eqI simp: ltl3_equiv_ltl em_ltl)

end