theory Traces 
imports Main HOL.Lattices HOL.List 
begin

chapter ‹Traces and Definitive Prefixes›

section ‹Traces›

typedecl Σ
type_synonym 'a finite_trace = ‹'a list›
type_synonym 'a infinite_trace = ‹nat → 'a›
datatype 'a trace = Finite ‹'a finite_trace› | Infinite ‹'a infinite_trace›

fun thead :: ‹'a trace → 'a› where
  ‹thead (Finite t) = t ! 0›
| ‹thead (Infinite t) = t 0›

fun append :: ‹'a trace → 'a trace → 'a trace› (infixr ‹⌢› 80) where
  ‹(Finite t) ⌢ (Infinite ψ) = Infinite (λn. if n < length t then t!n else ψ (n - length t))›
| ‹(Finite t) ⌢ (Finite u) = Finite (t @ u)›
| ‹(Infinite t) ⌢ u = Infinite t›

definition ε :: ‹'a trace› where
  ‹ε = Finite []›

definition singleton :: ‹'a → 'a trace› where
  ‹singleton σ = Finite [σ]›

interpretation trace: monoid_list ‹(⌢)› ‹ε›
proof unfold_locales
  fix a :: ‹'a trace› show ‹ε ⌢ a = a›
    by (cases ‹a›; simp add: ε_def)
next
  fix a :: ‹'a trace› show ‹a ⌢ ε = a›
    by (cases ‹a›; simp add: ε_def)
next
  fix a b c :: ‹'a trace› show ‹(a ⌢ b) ⌢ c = a ⌢ (b ⌢ c)›
    apply (cases ‹a›; simp)
    apply (cases ‹b›; simp)
    apply (cases ‹c›; simp)
    apply (rule ext; simp)
    by (smt (verit, ccfv_threshold) 
            add.commute add_diff_inverse_nat add_less_cancel_left 
            nth_append trans_less_add2)
qed

lemma finite_empty_suffix: 
  assumes ‹Finite xs = Finite xs ⌢ t›
  shows ‹t = ε›
  using assms by (cases ‹t›) (simp_all add: ε_def)

lemma finite_empty_prefix: 
  assumes ‹Finite xs = t ⌢ Finite xs›
  shows ‹t = ε›
  using assms by (cases ‹t›) (simp_all add: ε_def)

lemma finite_finite_suffix: 
  assumes ‹Finite xs = Finite ys ⌢ t›
  obtains zs where ‹t = Finite zs›
  using assms by (cases ‹t›) (simp_all)

lemma finite_finite_prefix:
  assumes ‹Finite xs = t ⌢ Finite ys›
  obtains zs where ‹t = Finite zs›
  using assms by (cases ‹t›) (simp_all)

lemma append_is_empty:
  assumes ‹t ⌢ u = ε›
  shows   ‹t = ε›
  and     ‹u = ε›
  using assms by (simp add: ε_def; cases ‹t›; cases ‹u›; simp)+

fun ttake :: ‹nat → 'a trace → 'a finite_trace› where
  ‹ttake k (Finite xs) = take k xs›
| ‹ttake k (Infinite xs) = map xs [0..<k] ›


definition itdrop :: ‹nat → 'a infinite_trace → 'a infinite_trace› where
  ‹itdrop k xs = (λi. xs (i + k))›

lemma itdrop_itdrop[simp]: ‹itdrop i (itdrop j x) = itdrop (i + j) x›
  by (simp add: itdrop_def add.commute add.left_commute)

lemma itdrop_zero[simp]: ‹itdrop 0 x = x›
  by (simp add: itdrop_def)


fun tdrop :: ‹nat → 'a trace → 'a trace› where
  ‹tdrop k (Finite xs) = Finite (drop k xs)›
| ‹tdrop k (Infinite xs) = Infinite (itdrop k xs) ›

lemma ttake_simp[simp]: ‹ttake (length xs) (Finite xs ⌢ t) = xs›
  by (cases ‹t›, auto intro:  list_eq_iff_nth_eq[THEN iffD2])

lemma ttake_tdrop[simp]: ‹Finite (ttake k t) ⌢ tdrop k t = t›
  by (cases ‹t›, auto simp: itdrop_def)

definition prefixes :: ‹'a trace → 'a trace set› (‹↓ _› [80] 80) where
  ‹↓ t = { u | u v. t = u ⌢ v }›

definition extensions :: ‹'a trace → 'a trace set› (‹↑ _› [80] 80) where
  ‹↑ t = { t ⌢ u | u. True }›

lemma prefixes_extensions: ‹t ∈ ↓ u ⟷ u ∈ ↑ t›
  unfolding prefixes_def extensions_def by simp

interpretation prefixes: order ‹λ t u. t ∈ ↓ u› ‹λ t u. t ∈ ↓ u ∧ t ≠ u›
proof 
  (* Reflexivity *)
  fix x :: ‹'a trace›
  show ‹x ∈ ↓ x›
    unfolding prefixes_def
    by (simp, metis trace.right_neutral)
next
  (* Strict Ordering *)
  fix x y :: ‹'a trace›
  show ‹(x ∈ ↓ y ∧ x ≠ y) = (x ∈ ↓ y ∧ ¬ y ∈ ↓ x)›
    unfolding prefixes_def
    by (simp, metis append.simps(3) append_is_empty(1) finite_empty_suffix 
                    trace.assoc trace.exhaust)
next
  (* Antisymmetry *)
  fix x y :: ‹'a trace›
  assume assms: ‹x ∈ ↓ y› ‹y ∈ ↓ x›
  show ‹x = y›
  proof (cases ‹y›)
    case Finite note yfinite = this 
    show ‹?thesis›
    proof (cases ‹x›)
      case Finite
      with assms(2) obtain z where ‹x = y ⌢ z›
        unfolding  prefixes_def
        by auto
      with assms(1) yfinite show ‹?thesis›
        unfolding  prefixes_def
        by (force simp: trace.assoc dest: finite_empty_suffix append_is_empty)
    qed (smt (verit, del_insts) CollectD append.simps(3) assms(1) prefixes_def)
  qed (smt (verit, del_insts) CollectD append.simps(3) assms(2) prefixes_def)
next
  (* Transitivity *)
  fix x y z :: ‹'a trace›
  assume ‹x ∈ ↓ y› ‹y ∈ ↓ z›
  then show ‹x ∈ ↓ z›
  unfolding  prefixes_def by (force simp: trace.assoc)
qed

lemma prefixes_empty_least : ‹ε ∈ ↓ t›
  by (simp add: prefixes_def)
  
lemma prefixes_infinite_greatest : ‹Infinite x ∈ ↓ t ==> t = Infinite x›
  by (simp add: prefixes_def)



lemma prefixes_finite : ‹Finite xs ∈ ↓ Finite ys ⟷ (∃ zs. ys = xs @ zs)›
proof (rule iffI)
  show ‹Finite xs ∈ ↓ Finite ys ==> ∃zs. ys = xs @ zs›
    using finite_finite_suffix by (fastforce simp: prefixes_def)
next
  show ‹∃zs. ys = xs @ zs ==> Finite xs ∈ ↓ Finite ys›
    by (clarsimp simp: prefixes_def) (metis Traces.append.simps(2))
qed

lemma ttake_take : ‹take n (ttake m t) = ttake (min n m) t›
  by (cases ‹t›) (simp_all add: min_def take_map)

lemma tdrop_tdrop : ‹tdrop n (tdrop m t) = tdrop (n + m) t›
  by (cases ‹t›) (simp_all add: add.commute add.left_commute)


lemma tdrop_mono: ‹t ∈ ↓ u ==> tdrop k t ∈ ↓ tdrop k u›
proof -
  { fix v assume A: ‹u = t ⌢ v› then have ‹∃va. tdrop k (t ⌢ v) = tdrop k t ⌢ va ›
  proof (cases ‹t›; cases ‹v›)
    fix x1 x2 assume ‹t = Finite x1› and ‹v = Finite x2› with A show ‹?thesis›
      by (simp, metis Traces.append.simps(2))
  next
    fix x1 x2 assume ‹t = Finite x1› and ‹v = Infinite x2› with A
     have ‹tdrop k (t ⌢ v) = tdrop k t ⌢ Infinite (itdrop (k - length x1) x2) ›
      apply simp
      apply (rule ext)
      apply clarsimp
      apply (rule conjI)      
       apply (simp add: add.commute itdrop_def less_diff_conv)
      by (smt (z3) add.commute add_diff_cancel_left' add_diff_inverse_nat diff_is_0_eq' 
                   diff_right_commute itdrop_def linorder_not_less nat_less_le)
    then show ‹∃va. tdrop k (t ⌢ v) = tdrop k t ⌢ va›
      by auto
  qed auto } note A = this
  assume ‹t ∈ ↓ u› with A show ?thesis unfolding prefixes_def by clarsimp
qed

lemma ttake_finite_prefixes : ‹Finite xs ∈ ↓ t ⟷ xs = ttake (length xs) t›
proof (rule iffI)
  show ‹Finite xs ∈ ↓ t ==> xs = ttake (length xs) t›
    by (clarsimp simp: prefixes_def)
next
  show ‹xs = ttake (length xs) t ==> Finite xs ∈ ↓ t›
    unfolding prefixes_def using ttake_tdrop
    by (metis (full_types) mem_Collect_eq)
qed

lemma ttake_prefixes : ‹a ≤ b ==> Finite (ttake a t) ∈ ↓ Finite (ttake b t)›
  by (cases ‹t›; simp add: ttake_finite_prefixes min_def take_map)

lemma finite_directed:
assumes ‹ Finite xs ∈ ↓ t › ‹ Finite ys ∈ ↓ t ›
shows ‹ ∃zs. (xs = ys @ zs) ∨ (ys = xs @ zs) ›
proof (cases ‹length xs > length ys›)
  case True
  with assms show ‹?thesis›
    apply (simp add: ttake_finite_prefixes)
    using ttake_prefixes[simplified prefixes_finite]
    by (metis less_le_not_le) 
next
  case False
  from assms this[THEN leI] show ‹?thesis›
    apply (simp add: ttake_finite_prefixes)
    using ttake_prefixes[simplified prefixes_finite]
    by (metis)
qed


lemma prefixes_directed: ‹u ∈ ↓ t ==> v ∈ ↓ t ==> u ∈ ↓ v ∨ v ∈ ↓ u›
proof (cases ‹v›; cases ‹u›)
  { fix a b assume ‹Finite a ∈ ↓ t› ‹Finite b ∈ ↓ t›
  then have ‹Finite a ∈ ↓ Finite b ∨ Finite b ∈ ↓ Finite a›
    using finite_directed prefixes_finite by blast } note X = this
  fix a b show ‹u ∈ ↓ t ==> v ∈ ↓ t ==> v = Finite a ==> u = Finite b ==> u ∈ ↓ v ∨ v ∈ ↓ u›
    using X by auto
qed (auto simp: prefixes_def dest: prefixes_infinite_greatest)

interpretation extensions: order ‹λ t u. t ∈ ↑ u› ‹λ t u. t ∈ ↑ u ∧ t ≠ u›
proof
qed (auto simp: prefixes_extensions[THEN sym] dest: prefixes.leD intro:prefixes.order.trans)

lemma extensions_infinite[simp]: ‹↑ Infinite xs = { Infinite xs }›
  by (simp add: extensions_def)

lemma extensions_empty[simp]: ‹↑ ε = UNIV›
  by (simp add: extensions_def)

lemma prefixes_empty: ‹↓ ε = {ε}›
  apply (clarsimp simp add: set_eq_iff ε_def prefixes_def)
  apply (rule iffI)
  apply (metis ε_def append_is_empty(1))
  by (metis ε_def trace.left_neutral)


section ‹Prefix Closure›

definition prefix_closure :: ‹'a trace set → 'a trace set› (‹↓_s _› [80] 80) where
  ‹↓_s X = (∪ t ∈ X. prefixes t) ›

lemma prefix_closure_subset: ‹X ⊆ ↓_s X›
  unfolding prefix_closure_def
  by auto 

lemma prefix_closure_infinite: ‹Infinite x ∈ ↓_s X ⟷ Infinite x ∈ X›
proof
  assume ‹Infinite x ∈ ↓_s X› then show ‹Infinite x ∈ X›
    by (metis UN_E prefix_closure_def prefixes_infinite_greatest)
next
  assume ‹Infinite x ∈ X› then show ‹Infinite x ∈ ↓_s X›
    by (meson in_mono prefix_closure_subset)
qed

lemma prefix_closure_idem: ‹↓_s ↓_s X = ↓_s X›
  unfolding prefix_closure_def
  using prefixes.order.trans by blast

lemma prefix_closure_mono: ‹X ⊆ Y ==> ↓_s X ⊆ ↓_s Y›
  unfolding prefix_closure_def
  by blast

lemma prefix_closure_union_distrib: ‹↓_s (X ∪ Y) = ↓_s X ∪ ↓_s Y›
  unfolding prefix_closure_def
  by simp

lemma prefix_closure_Union_distrib: ‹↓_s (∪ S) = ∪ (prefix_closure ` S)›
  unfolding prefix_closure_def
  by simp

lemma prefix_closure_Inter: ‹↓_s (∩ (prefix_closure ` S)) = ∩ (prefix_closure ` S) ›
  unfolding prefix_closure_def
  using prefixes.dual_order.trans by fastforce

lemma prefix_closure_inter: ‹↓_s (↓_s X ∩ ↓_s Y) = ↓_s X ∩ ↓_s Y›
  by (rule prefix_closure_Inter[where S = ‹{X,Y}›, simplified])

lemma prefix_closure_UNIV: ‹↓_s UNIV = UNIV›
  unfolding prefix_closure_def by blast

lemma prefix_closure_empty: ‹↓_s {} = {}›
  unfolding prefix_closure_def by blast

lemma prefix_closure_extensions: ‹ ↓_s (↑ t) = ↑ t ∪ ↓ t›
  by (force intro: prefix_closure_subset dest: prefixes_directed
            simp: prefixes_extensions[THEN sym] prefix_closure_def)

lemma prefix_closure_prefixes: ‹↓_s (↓ t) = ↓ t›
  unfolding prefix_closure_def
  by (force intro: prefixes.dual_order.trans)

section ‹Definitive Prefixes›

definition dprefixes :: ‹'a trace set → 'a trace set›  (‹↓_d _› [80] 80) where
  ‹↓_d X = { t | t. ↑ t ⊆ ↓_s X }›

lemma dprefixes_are_prefixes : ‹↓_d X ⊆ ↓_s X›
  unfolding dprefixes_def
  using extensions.order.refl by blast

lemma prefix_closure_dprefixes : ‹↓_s (↓_d X) ⊆ ↓_s X›
  using dprefixes_are_prefixes prefix_closure_idem prefix_closure_mono 
  by blast

lemma dprefixes_idem: ‹↓_d ↓_d X = ↓_d X›
proof
  show ‹↓_d ↓_d X ⊆ ↓_d X›
    using prefix_closure_dprefixes 
    by (force simp: dprefixes_def)
next
  show ‹↓_d X ⊆ ↓_d ↓_d X›
    using extensions.order.trans prefix_closure_subset 
    by (force simp: dprefixes_def)
qed

lemma dprefixes_contains_extensions: ‹t ∈ ↓_d X ==> ↑ t ⊆ ↓_d X›
  unfolding dprefixes_def
  using extensions.dual_order.trans by auto

lemma dprefixes_infinite: ‹Infinite x ∈ ↓_d X ⟷ Infinite x ∈ X›
proof
  show ‹Infinite x ∈ X ==> Infinite x ∈ ↓_d X›
  unfolding dprefixes_def
  using prefix_closure_subset by fastforce
next
  show ‹Infinite x ∈ ↓_d X ==> Infinite x ∈ X›
  unfolding dprefixes_def
  by (clarsimp simp: prefix_closure_infinite)
qed


lemma dprefixes_UNIV: ‹↓_d UNIV = UNIV›
  unfolding dprefixes_def
  using prefix_closure_UNIV by force

lemma dprefixes_empty: ‹↓_d {} = {}›
  unfolding dprefixes_def
  using prefix_closure_empty by blast

lemma dprefixes_Inter_distrib: ‹↓_d (∩ S) ⊆ ∩ (dprefixes ` S)›
  unfolding dprefixes_def prefix_closure_def
  by auto

lemma dprefixes_Inter: ‹↓_d (∩ (dprefixes ` S)) = ∩ (dprefixes ` S)›
proof
  show ‹∩ (dprefixes ` S) ⊆ ↓<sub>d</sub> ∩ (dprefixes ` S)›
    unfolding dprefixes_def prefix_closure_def
    using prefixes.order.refl extensions.dual_order.trans 
    by force
next
  show ‹↓_d ∩ (dprefixes ` S) ⊆ ∩ (dprefixes ` S)›
    using dprefixes_idem  dprefixes_Inter_distrib 
    by blast
qed

lemma dprefixes_mono: 
  assumes ‹X ⊆ Y›
  shows ‹↓_d X ⊆ ↓_d Y›
  using assms
  apply (simp add: dprefixes_def)
  apply (simp add: prefix_closure_def)
  apply (rule subsetI)
  using prefixes_extensions by blast


lemma dprefixes_inter: ‹↓_d (↓_d X ∩ ↓_d Y) = (↓_d X ∩ ↓_d Y)›
  by (rule dprefixes_Inter[where S = ‹{X,Y}›, simplified])

lemma dprefixes_inter_distrib: ‹↓_d (X ∩ Y) ⊆ ↓_d X ∩ ↓_d Y›
  using dprefixes_Inter_distrib[where S = ‹{X,Y}›] by auto

section ‹Definitive Sets›

definition definitive:: ‹'a trace set → bool› where
  ‹definitive X ⟷ ↓_d X = X›

lemma definitive_image: ‹∀X ∈ S. definitive X ==> dprefixes ` S = S›
  unfolding definitive_def by auto

lemma definitive_dprefixes: ‹definitive (↓_d X)›
  unfolding definitive_def by (rule dprefixes_idem)

lemma definitive_contains_extensions: ‹definitive X ==> t ∈ X ==> ↑ t ⊆ X›
  unfolding definitive_def using dprefixes_contains_extensions by blast

lemma definitive_UNIV: ‹definitive UNIV›
  unfolding definitive_def by (rule dprefixes_UNIV)

lemma definitive_empty: ‹definitive {}›
  unfolding definitive_def by (rule dprefixes_empty)

lemma definitive_Inter: ‹∀X ∈ S. definitive X ==> definitive (∩ S)›
  unfolding definitive_def using dprefixes_Inter definitive_image[simplified definitive_def]
  by metis

lemma definitive_inter: ‹definitive X ==> definitive Y ==> definitive (X ∩ Y)›
  using definitive_Inter[where S = ‹{X,Y}›, simplified] by blast

lemma definitive_infinite_extension:
  assumes ‹definitive X› and ‹t ∈ X›
  shows ‹∃ f. Infinite f ∈ X ∧ t ∈ ↓ Infinite f›
using assms proof (cases ‹t›)
  case (Finite xs) then show ‹?thesis›
    apply (intro exI[where x=‹λn. if n < length xs then xs!n else undefined›])
    by (force simp:   prefixes_extensions[THEN sym] prefixes_def 
              intro!: definitive_contains_extensions[THEN subsetD, OF assms] 
              intro:  exI[where x=‹Infinite (λ_. undefined)›])
qed auto

lemma definitive_elemI:
  assumes ‹definitive X› ‹↑ t ⊆ ↓_s X›
  shows ‹t ∈ X›
  using assms
  by (auto simp add: definitive_def dprefixes_def)


definition dUnion :: ‹'a trace set set → 'a trace set› (‹∪_d›) where
  ‹∪_d X = ↓_d ∪ X›

abbreviation dunion :: ‹'a trace set → 'a trace set → 'a trace set›  (infixl ‹∪_d› 65) where
  ‹X ∪_d Y ≡ ∪_d {X,Y}›

lemma dprefixes_dUnion: ‹↓_d ∪_d S = ∪_d S›
  by (simp add: dUnion_def dprefixes_idem)

lemma definitive_dUnion: ‹definitive (∪_d S)›
  by (simp add: dprefixes_dUnion definitive_def)

lemma dUnion_contains_dprefixes: ‹t ∈ S ==> ↓_d t ⊆ ∪_d S›
  by (auto simp: dUnion_def dprefixes_def prefix_closure_def)

lemma dUnion_contains_definitive: ‹X ∈ S ==> definitive X ==> X ⊆ ∪_d S›
  unfolding definitive_def
  using dUnion_contains_dprefixes by blast

lemma dUnion_empty[simp]: ‹∪_d {} = {}›
  unfolding dUnion_def
  by (simp add: dprefixes_empty)

lemma dUnion_least_dprefixes: ‹(∧X. X ∈ S ==> X ⊆ ↓_d Z) ==> ↓_d (∪ (dprefixes ` S)) ⊆ ↓_d Z›
  unfolding dprefixes_def prefix_closure_def
  by (simp add: subset_iff, meson extensions.order_refl prefixes.order.trans)

lemma dUnion_least_definitive: 
  assumes all_defn: ‹∀X ∈ S. definitive X›
  shows ‹(∧X. X ∈ S ==> X ⊆ Z) ==> definitive Z ==> ↓_d ∪ S ⊆ Z›
  using  definitive_image[OF all_defn,THEN sym] dUnion_least_dprefixes definitive_def
  by metis

section ‹A type for definitive sets›

typedef 'a dset = ‹{p :: 'a trace set. definitive p }›
  using definitive_UNIV by blast

setup_lifting type_definition_dset

lift_definition Inter_dset :: ‹'a dset set → 'a dset› (‹⊓›) is ‹λ ss. ∩ ss›
  by (simp add: definitive_Inter)

abbreviation inter_dset :: ‹'a dset → 'a dset → 'a dset›  (infixl ‹⊓› 66)  where
  ‹X ⊓ Y ≡ ⊓ {X,Y}›

lift_definition Union_cset :: ‹'a dset set → 'a dset› (‹⊔›) is ‹λ ss. ∪_d ss›
  by (rule definitive_dUnion)

abbreviation union_dset :: ‹'a dset → 'a dset → 'a dset›  (infixl ‹⊔› 65)  where
  ‹X ⊔ Y ≡ ⊔ {X,Y}›

lift_definition empty_dset :: ‹'a dset› (‹∅›) is ‹{}›
  by (rule definitive_empty)

lift_definition univ_dset :: ‹'a dset› (‹Σ∞›) is ‹UNIV›
  by (rule definitive_UNIV)

lift_definition subset_dset :: ‹'a dset → 'a dset → bool› (infix ‹⊑› 50) is ‹(⊆)›
  done

lift_definition strict_subset_cset :: ‹'a dset → 'a dset → bool›  (infix ‹⊏› 50) is ‹(⊂)›
  done

lift_definition in_dset :: ‹'a trace → 'a dset → bool› is ‹(∈)›
  done

lift_definition notin_dset :: ‹'a trace → 'a dset → bool› is ‹(∉)›
  done



lemma in_dset_ε: ‹in_dset ε A ==> A = Σ∞›
  apply (transfer)
  using definitive_contains_extensions extensions_empty by blast

lemma in_dset_UNIV: ‹in_dset x Σ∞›
  by (transfer, simp)

lemma in_dset_subset: ‹A ⊑ B ==> in_dset x A ==> in_dset x B›
  by (transfer, auto)

lemma in_dset_inter: ‹in_dset x A ==> in_dset x B ==> in_dset x (A ⊓ B)›
  by (transfer, simp)


interpretation dset: complete_lattice ‹⊓› ‹⊔› ‹(⊓)› ‹(⊑)› ‹(⊏)› ‹(⊔)› ‹∅› ‹Σ∞›
proof (unfold_locales;transfer)
  fix X Y Z :: ‹'a trace set› assume ‹definitive X› ‹definitive Y› ‹definitive Z›
  then show ‹ Y ⊆ X ==> Z ⊆ X ==> (Y ∪_d Z) ⊆ X›
    by (metis dUnion_def dUnion_least_definitive insert_iff singletonD)
next
  fix A :: ‹'a trace set set› and Z :: ‹'a trace set›
  assume ‹∀X∈A. definitive X› ‹definitive Z› ‹(∧X. definitive X ==> X ∈ A ==> X ⊆ Z)›
  then show ‹∪_d A ⊆ Z›
    by (simp add: dUnion_def dUnion_least_definitive)
qed (auto simp: dUnion_contains_definitive)

section ‹Isomorphism of definitive sets and LTL properties›

definition infinites :: ‹'a trace set → 'a infinite_trace set› where
  ‹infinites X = (∪x ∈ X. case x of Finite xs → {} | Infinite xs → {xs})›

lemma infinites_alt: ‹Infinite ` infinites A = A ∩ range Infinite›
unfolding set_eq_iff proof 
  fix x { assume ‹ (x ∈ Infinite ` infinites A)› hence ‹ (x ∈ A ∩ range Infinite) ›
    by (clarsimp simp: infinites_def split!: trace.split_asm)
  } moreover { assume ‹ (x ∈ A ∩ range Infinite) › hence ‹ (x ∈ Infinite ` infinites A) ›
      by (force simp: infinites_def split!: trace.split intro!: imageI)
  } ultimately show ‹ (x ∈ Infinite ` infinites A) = (x ∈ A ∩ range Infinite)›
    by blast
qed

lemma infinites_append_right: ‹t ⌢ Infinite ψ ∈ range Infinite›
  by (cases ‹t›; auto)

lemma infinites_prefix_closure:
  assumes ‹definitive X›
  shows ‹↓_s Infinite ` infinites X = ↓_s X›
  unfolding prefix_closure_def infinites_def
  using definitive_infinite_extension[OF assms] prefixes.order.trans 
  by (force split: trace.split_asm)

lemma infinites_UNIV[simp]: ‹infinites UNIV = UNIV›
 by (auto simp: infinites_def split: trace.split)

lemma infinites_empty[simp]: ‹infinites {} = {}›
  by (auto simp: infinites_def)
 
lemma infinites_Inter: ‹infinites (∩ S) = ∩ (infinites ` S)›
  unfolding infinites_def
  apply (rule set_eqI; rule iffI)
   apply (force)
   apply (simp split: trace.split trace.split_asm)
  by (metis InterI trace.distinct(1) trace.exhaust trace.inject(2))

lemma infinites_Union: ‹infinites (∪ S) = ∪ (infinites ` S)›
  unfolding infinites_def
  by auto

lemma infinites_dprefixes: ‹infinites (↓_d X) = infinites X›
  unfolding infinites_def
   by (force simp: dprefixes_infinite split: trace.split trace.split_asm)

lemma infinites_dprefixes_Infinite: ‹infinites (↓_d Infinite ` X) = X›
proof
  show ‹infinites (↓<sub>d</sub> Infinite ` X) ⊆ X›
    unfolding infinites_def
    using prefixes_infinite_greatest
    by (force split: trace.split_asm simp: dprefixes_def prefix_closure_def)
next
  show ‹X ⊆ infinites (↓_d Infinite ` X)›
    by (force simp: infinites_def dprefixes_def prefix_closure_def split: trace.split)
qed

lift_definition property :: ‹'a dset → 'a infinite_trace set› is ‹infinites›
  done

lift_definition definitives :: ‹'a infinite_trace set → 'a dset› is ‹λx. ↓_d (Infinite ` x)›
  by (rule definitive_dprefixes)

lemma property_inverse: ‹property (definitives X) = X›
  by (transfer, simp add: infinites_dprefixes_Infinite)

lemma definitives_inverse: ‹definitives (property X) = X›
proof (rule dset.order_antisym)
  show ‹definitives (property X) ⊑ X›
    by (transfer, force simp: dprefixes_def infinites_prefix_closure 
                        intro: definitive_elemI)
next
  show ‹X ⊑ definitives (property X)›
    apply transfer
    using definitive_contains_extensions definitive_infinite_extension 
    by (force simp: dprefixes_def prefix_closure_def infinites_def)
qed

lemma definitives_mono: ‹A ⊆ B ==> definitives A ⊑ definitives B›
  by (transfer, metis dprefixes_inter_distrib image_mono inf.order_iff le_infE)

lemma property_mono: ‹A ⊑ B ==> property A ⊆ property B›
  by (transfer, auto simp: infinites_def)

lemma definitives_reflecting: ‹definitives A ⊑ definitives B ==> A ⊆ B›
  using property_inverse property_mono by metis

lemma completions_reflecting: ‹property A ⊆ property B ==> A ⊑ B›
  using definitives_inverse definitives_mono by metis

lemma property_Inter: ‹property (⊓ S) = ∩ (property ` S)›
  by (transfer, simp add: infinites_Inter)

lemma property_Union: ‹property (⊔ S) = ∪ (property ` S)›
  by (transfer, simp add: dUnion_def infinites_dprefixes infinites_Union)



interpretation dset: complete_distrib_lattice ‹⊓› ‹⊔› ‹(⊓)› ‹(⊑)› ‹(⊏)› ‹(⊔)› ‹∅› ‹Σ∞›
  by (unfold_locales)
     (auto intro: completions_reflecting simp add: property_Inter property_Union INF_SUP_set)


definition iprepend :: ‹'a infinite_trace set → 'a infinite_trace set› where
  ‹iprepend X = {t. itdrop 1 t ∈ X }›

lemma iprepend_itdrop: ‹itdrop k x ∈ iprepend B ⟷ itdrop (Suc k) x ∈ B›
  by (simp add: iprepend_def)

lemmas iprepend_itdrop_0[simp] = iprepend_itdrop[where k = ‹0›,simplified]

definition prepend' :: ‹'a trace set → 'a trace set› where
  ‹prepend' X = {t. tdrop 1 t ∈ X }›

lemma trace_uncons_cases [case_names Cons Nil]: 
  assumes ‹∧σ t. x = singleton σ ⌢ t ==> P›
  and ‹x = ε ==> P›
  shows ‹P›
proof (cases ‹x›)
  case (Finite xs)
  then show ‹?thesis›
    by (cases ‹xs›; 
        force simp: assms(2)[simplified ε_def] 
              intro: assms(1)[where t = ‹Finite ts› for ts,
                     simplified singleton_def append.simps List.append.simps])
next
  case (Infinite f) note A = this
  have ‹f = (λn. if n = 0 then [f 0] ! n else (f ∘ Suc) (n - length [f 0]))›
    by (rule ext, simp)
  with A show ‹?thesis›
    using assms(1)[where σ = ‹f 0› and t = ‹Infinite (f ∘ Suc)›,
                   simplified singleton_def append.simps, simplified]
    by simp
qed

lemma append_prefixes_left: ‹a ∈ ↓ b ==> c ⌢ a ∈ ↓ c ⌢ b›
  by (simp add: prefixes_def) (metis trace.assoc)

lemma tdrop_singleton_append[simp]: ‹tdrop (Suc n) (singleton σ ⌢ t) = tdrop n t›
  by (cases ‹t›, simp_all add: singleton_def itdrop_def)
lemma tdrop_zero[simp]: ‹tdrop 0 t = t›
  by (cases ‹t›; simp)
lemma tdrop_ε[simp]: ‹tdrop k ε = ε›
  by (simp add: ε_def)

lemma prepend'_prefix_closure: ‹↓_s (prepend' X) ⊆ prepend' (↓_s X)›
proof (rule subsetI)
  fix x 
  assume A: ‹ x ∈ ↓_s prepend' X›
  show ‹x ∈ prepend' (↓_s X) ›
  proof (cases ‹x› rule: trace_uncons_cases)
    case (Cons σ t)
    with A show ‹?thesis›
      unfolding prefix_closure_def prepend'_def prefixes_def 
      by (fastforce simp: trace.assoc)
  next
    case Nil
    with A show ‹?thesis›
      unfolding prefix_closure_def prepend'_def
      by (force simp: prefixes_empty_least)
  qed
qed

lemma prepend'_dprefixes : 
assumes ‹definitive X›
shows ‹↓_d prepend' X = prepend' X›
proof
  show ‹↓_d prepend' X ⊆ prepend' X›
  proof (rule subsetI)
    fix x assume A: ‹x ∈ ↓_d prepend' X› show ‹x ∈ prepend' X›
    proof (cases ‹x› rule: trace_uncons_cases)
      case (Cons σ t)
      with A show ‹?thesis›
        unfolding dprefixes_def
        apply (subst assms[simplified definitive_def, THEN sym])
        apply (clarsimp dest!: subset_trans[OF _ prepend'_prefix_closure])
        using append_prefixes_left 
        by (force simp: dprefixes_def prepend'_def prefix_closure_def subset_iff 
                        prefixes_extensions[THEN sym])
    next
      case Nil
      with A show ‹?thesis›
        apply (subst assms[simplified definitive_def, THEN sym])
        apply (clarsimp simp: prefixes_empty_least prefixes_def dprefixes_def 
                              prepend'_def prefix_closure_def subset_iff
                              prefixes_extensions[THEN sym])
        by (metis tdrop_singleton_append tdrop_zero trace.assoc)
    qed
  qed
next
  show ‹prepend' X ⊆ ↓_d prepend' X›
  proof (rule subsetI)
    fix x assume A: ‹x ∈ prepend' X› show ‹x ∈ ↓_d prepend' X›
    proof (cases ‹x› rule: trace_uncons_cases)
      case (Cons σ t)
      with A show ‹?thesis›
        by (clarsimp simp: dprefixes_def prefixes_def prepend'_def 
                              prefix_closure_def prefixes_extensions[THEN sym])
           (metis (mono_tags, lifting) assms definitive_contains_extensions 
                  mem_Collect_eq prefixes_def prefixes_extensions subset_eq 
                  tdrop_singleton_append tdrop_zero trace.assoc)
    next
      case Nil
      with A show ‹?thesis›
        using assms definitive_contains_extensions 
        by (force simp: dprefixes_def prepend'_def prefix_closure_def)
    qed
  qed
qed

lemma prepend'_definitive : 
  assumes ‹definitive X›
  shows ‹definitive (prepend' X)›
  unfolding definitive_def using assms
  by (rule prepend'_dprefixes)

lift_definition prepend :: ‹'a dset → 'a dset› is ‹prepend'›
  by (rule prepend'_definitive)

lemma prepend_Inter: ‹⊓ (prepend ` S) = prepend (⊓ S)›
  apply transfer
  by (auto simp add: prepend'_def)

lemma in_dset_prependD: ‹in_dset (Finite [a] ⌢ x) (prepend A) ==> in_dset x A›
  by (transfer, metis One_nat_def Traces.singleton_def mem_Collect_eq prepend'_def 
                      tdrop_singleton_append tdrop_zero)

lemma in_dset_prependI: ‹in_dset x A ==> in_dset (Finite [a] ⌢ x) (prepend A)›
  by (transfer, metis One_nat_def Traces.singleton_def mem_Collect_eq prepend'_def 
                      tdrop_singleton_append tdrop_zero)

lemma prepend'_mono: 
  assumes ‹A ⊆ B›
  shows   ‹prepend' A ⊆ prepend' B›
  using assms unfolding prepend'_def
  by blast

lemma property_prepend: ‹property (prepend X) = iprepend (property X)›
  apply transfer
  by (clarsimp simp: definitive_def infinites_def prepend'_def 
               split!: trace.split_asm trace.split intro!: set_eqI; 
      blast)

lemma iprepend_Union: ‹∪ (iprepend ` S) = iprepend (∪ S)›
  by fastforce

lemma definitives_inverse_eqI: ‹definitives (property X) = definitives (property Y) ==> X = Y›
  by (simp add: definitives_inverse)

lemma prepend_Union: ‹⊔ (prepend ` S) = prepend (⊔ S)›
  apply (rule definitives_inverse_eqI)
  apply (simp add: property_Union property_prepend)
  by (metis UN_extend_simps(10) iprepend_Union)

lemma non_empty_trace: ‹ x ≠ ε ⟷ (∃σ x'. x = Finite [σ] ⌢ x')›
  apply (cases ‹x› rule: trace_uncons_cases; clarsimp)
   apply (metis Traces.singleton_def ε_def append_is_empty(1) not_Cons_self2 trace.inject(1))
  by (metis ε_def append_is_empty(1) list.discI trace.inject(1))

lemma thead_append: ‹x ≠ ε ==> thead (x ⌢ y) = thead x›
  by (cases ‹x›; cases ‹y›; simp add: ε_def nth_append)

lemma thead_prefix: ‹ x ∈ ↓ y ==> x ≠ ε ==> thead x = thead y›
  apply (simp add: prefixes_def non_empty_trace)
  using thead_append [where x = ‹Finite [_]›, simplified ε_def, simplified]
  by (metis append_is_empty(1) thead_append)

lemma compr'_inter_thead: 
    ‹↓_d {x. x ≠ ε ∧ P (thead x)} ∩ ↓_d {x. x ≠ ε ∧ Q (thead x)}
 = ↓_d {x. x ≠ ε ∧ P (thead x) ∧ Q (thead x)}›
proof (rule antisym)
{ fix x t
  assume ‹∀t. x ∈ ↓ t ⟶ (∃x. x ≠ ε ∧ P (thead x) ∧ t ∈ ↓ x)›
  and    ‹∀t. x ∈ ↓ t ⟶ (∃x. x ≠ ε ∧ Q (thead x) ∧ t ∈ ↓ x)›
  and    ‹x ∈ ↓ t›
  then have ‹ ∃x. x ≠ ε ∧ P (thead x) ∧ Q (thead x) ∧ t ∈ ↓ x›
    by (cases ‹t = ε›; fastforce dest: thead_prefix simp: prefixes_empty prefixes_empty_least)
} then show ‹↓_d {x. x ≠ ε ∧ P (thead x)} ∩ ↓_d {x. x ≠ ε ∧ Q (thead x)} ⊆ ↓_d {x. x ≠ ε ∧ P (thead x) ∧ Q (thead x)}›
  by (clarsimp simp: set_eq_iff subset_iff dprefixes_def prefix_closure_def prefixes_extensions[THEN sym])
next
{ fix x
  assume ‹ ∀t. x ∈ ↓ t ⟶ (∃x. x ≠ ε ∧ P (thead x) ∧ Q (thead x) ∧ t ∈ ↓ x)›
  then have ‹(∀t. x ∈ ↓ t ⟶ (∃x. x ≠ ε ∧ P (thead x) ∧ t ∈ ↓ x)) ∧
 (∀t. x ∈ ↓ t ⟶ (∃x. x ≠ ε ∧ Q (thead x) ∧ t ∈ ↓ x))›
    by fastforce }
  then show ‹↓_d {x. x ≠ ε ∧ P (thead x)} ∩ ↓_d {x. x ≠ ε ∧ Q (thead x)} ⊇ ↓_d {x. x ≠ ε ∧ P (thead x) ∧ Q (thead x)}›
  by (clarsimp simp: set_eq_iff subset_iff dprefixes_def prefix_closure_def prefixes_extensions[THEN sym])
qed

lift_definition compr :: ‹('a trace → bool) → 'a dset› is ‹λp. ↓_d {x. p x }›
  by (rule definitive_dprefixes)


lift_definition complement :: ‹'a dset → 'a dset› is ‹λp. ↓_d (range Infinite - p)›
  by (rule definitive_dprefixes)


lemma property_complement[simp]: ‹property (complement X) = UNIV - property X›
  by (transfer, force simp: infinites_dprefixes[simplified infinites_def] infinites_def 
                      split: trace.split_asm trace.split)

end