Quelle  Hiding.thy

(*<*)
―‹ ********************************************************************
 * Project : HOL-CSP - A Shallow Embedding of CSP in Isabelle/HOL
 * Version : 2.0
 *
 * Author : Benoît Ballenghien, Safouan Taha, Burkhart Wolff, Lina Ye.
 * (Based on HOL-CSP 1.0 by Haykal Tej and Burkhart Wolff)
 *
 * This file : Hiding operator
 *
 * Copyright (c) 2009 Université Paris-Sud, France
 * Copyright (c) 2025 Université Paris-Saclay, France
 *
 * All rights reserved.
 *
 * Redistribution and use in source and binary forms, with or without
 * modification, are permitted provided that the following conditions are
 * met:
 *
 * * Redistributions of source code must retain the above copyright
 * notice, this list of conditions and the following disclaimer.
 *
 * * Redistributions in binary form must reproduce the above
 * copyright notice, this list of conditions and the following
 * disclaimer in the documentation and/or other materials provided
 * with the distribution.
 *
 * * Neither the name of the copyright holders nor the names of its
 * contributors may be used to endorse or promote products derived
 * from this software without specific prior written permission.
 *
 * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
 * "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
 * LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
 * A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
 * OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
 * SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
 * LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
 * DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
 * THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
 * (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
 * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
 ******************************************************************************›
(*>*)


chapter‹The Hiding Operator›

(*<*)
theory  Hiding
  imports Process
begin
  (*>*)

section‹Preliminaries : primitives and lemmas›

abbreviation ‹trace_hide t A ≡ filter (λx. x ∉ A) t›

lemma Hiding_tickFree : ‹tF (trace_hide s (ev ` A)) ⟷ tF s›
  by (auto simp add: tickFree_def)

lemma Hiding_front_tickFree : ‹ftF s ==> ftF (trace_hide s (ev ` A))›
  apply (induct s; simp add: image_iff front_tickFree_Cons_iff)
  by (metis (no_types, lifting) filter.simps(1) front_tickFree_charn)

lemma trace_hide_union: ‹trace_hide t (A ∪ B) = trace_hide (trace_hide t A) B› by simp


lemma trace_hide_ev_union [simp] :
  ‹trace_hide t (ev ` (A ∪ B)) = trace_hide (trace_hide t (ev ` A)) (ev ` B)›
  apply (fold trace_hide_union)
  apply (rule arg_cong[where f = ‹λS. trace_hide t S›])
  by blast


abbreviation isInfHiddenRun :: ‹[nat ==> ('a, 'r) event_ptick list, ('a, 'r) process_ptick, 'a set] ==> bool›
  where ‹isInfHiddenRun f P A ≡ strict_mono f ∧ (∀i. f i ∈ T P) ∧
 (∀i. trace_hide (f i) (ev ` A) = trace_hide (f 0) (ev ` A))›

lemma isInfHiddenRun_1 :
  ‹isInfHiddenRun f P A ⟷ strict_mono f ∧ (∀i. f i ∈ T P) ∧
 (∀i. ∃t. f i = f 0 @ t ∧ set t ⊆ ev ` A)›
proof (intro iffI conjI; elim conjE, assumption?)
  assume * : ‹strict_mono f› ‹∀i. trace_hide (f i) (ev ` A) = trace_hide (f 0) (ev ` A)›
  show ‹∀i. ∃t. f i = f 0 @ t ∧ set t ⊆ ev ` A›
  proof (rule allI)
    fix i
    from "*"(1) obtain t where ‹f i = f 0 @ t›
      by (meson prefixE less_eq_nat.simps(1) strict_mono_less_eq)
    with "*"(2)[THEN spec, of i] have ‹set t ⊆ ev ` A›
      by simp (metis empty_filter_conv subset_code(1))
    with ‹f i = f 0 @ t› show ‹∃t. f i = f 0 @ t ∧ set t ⊆ ev ` A› by blast
  qed
next
  assume * : ‹∀i. ∃t. f i = f 0 @ t ∧ set t ⊆ ev ` A›
  show ‹∀i. trace_hide (f i) (ev ` A) = trace_hide (f 0) (ev ` A)›
  proof (rule allI)
    fix i
    from "*"[rule_format, of i] show ‹trace_hide (f i) (ev ` A) = trace_hide (f 0) (ev ` A)›
      by (elim exE, simp) (meson filter_False in_mono)
  qed
qed


abbreviation div_hide :: ‹('a, 'r) process_ptick ==> 'a set ==> ('a, 'r) event_ptick list set›
  where ‹div_hide P A ≡ {s. ∃t u. ftF u ∧ tF t ∧
 s = trace_hide t (ev ` A) @ u ∧
 (t ∈ D P ∨ (∃f. isInfHiddenRun f P A ∧ t ∈ range f))}›

lemma inf_hidden:
  ‹∃f. isInfHiddenRun f P A ∧ s ∈ range f›
  if ‹∀t. trace_hide t (ev ` A) = trace_hide s (ev ` A) ⟶ (t, ev ` A) ∉ F P› and ‹s ∈ T P›
proof (rule exI)
  define f where ‹f ≡ rec_nat s (λi t. let e = SOME e. e ∈ ev ` A ∧ t @ [e] ∈ T P in t @ [e])›
  have ‹strict_mono f› by (simp add: f_def strict_mono_def lift_Suc_mono_less_iff)
  moreover have ‹s ∈ range f› unfolding f_def by (metis (no_types, lifting) nat.rec(1) range_eqI)
  moreover have ‹f i ∈ T P ∧ trace_hide (f i) (ev ` A) = trace_hide s (ev ` A)› for i
  proof (induct i)
    show ‹f 0 ∈ T P ∧ trace_hide (f 0) (ev ` A) = trace_hide s (ev ` A)›
      by (simp add: f_def that(2))
  next
    fix i
    assume hyp : ‹f i ∈ T P ∧ trace_hide (f i) (ev ` A) = trace_hide s (ev ` A)›
    from is_processT5_S7[OF hyp[THEN conjunct1] that(1)[rule_format, OF hyp[THEN conjunct2]]]
    obtain e where $ : ‹e ∈ ev ` A› ‹f i @ [e] ∈ T P› by blast
    have ‹f (Suc i) = (let e = SOME e. e ∈ ev ` A ∧ f i @ [e] ∈ T P in f i @ [e])›
      by (simp add: f_def)
    thus ‹f (Suc i) ∈ T P ∧ trace_hide (f (Suc i)) (ev ` A) = trace_hide s (ev ` A)›
      by (simp add: hyp[THEN conjunct2]) (metis (no_types, lifting) "$" someI_ex)
  qed
  ultimately show ‹isInfHiddenRun f P A ∧ s ∈ range f› by simp
qed


lemma trace_hide_append :
  ‹s @ t = trace_hide u (ev ` A) ==>
 ∃s' t'. u = s' @ t' ∧ s = trace_hide s' (ev ` A) ∧ t = trace_hide t' (ev ` A)›
proof (induct u arbitrary: s t)
  case Nil
  thus ?case by simp
next
  case (Cons e u)
  show ?case
  proof (cases ‹e ∈ ev ` A›)
    assume ‹e ∈ ev ` A›
    with Cons.prems have ‹s @ t = trace_hide u (ev ` A)› by simp
    with Cons.hyps obtain s' t' where 
      ‹u = s' @ t'› ‹s = trace_hide s' (ev ` A)› ‹t = trace_hide t' (ev ` A)› by blast
    hence ‹e # u = (e # s') @ t' ∧ s = trace_hide (e # s') (ev ` A) ∧ t = trace_hide t' (ev ` A)›
      by (simp add: ‹e ∈ ev ` A›)
    thus ?case by blast
  next
    assume ‹e ∉ ev ` A›
    with Cons.prems consider ‹s = []› ‹t ≠ []› ‹hd t = e› ‹[] @ tl t = trace_hide u (ev ` A)›
      | ‹s ≠ []› ‹hd s = e› ‹tl s @ t = trace_hide u (ev ` A)› by (cases s) simp_all
    thus ?case
    proof cases
      show ‹[s = []; t ≠ []; hd t = e; [] @ tl t = trace_hide u (ev ` A)] ==> ?case›
        by (drule Cons.hyps) (metis Cons.prems append_Nil filter.simps(1))
    next
      show ‹[s ≠ []; hd s = e; tl s @ t = trace_hide u (ev ` A)] ==> ?case›
        by (drule Cons.hyps) (metis Cons.prems Cons_eq_appendI append_same_eq filter_append)
    qed
  qed
qed



section‹The Hiding Operator Definition›

lift_definition Hiding  :: ‹[('a, 'r) process_ptick ,'a set] ==> ('a, 'r) process_ptick› (infixl ‹\\› 69)
  is ‹λP A. ({(s, X). ∃t. s = trace_hide t (ev ` A) ∧ (t, X ∪ ev ` A) ∈ F P} ∪
 {(s, X). s ∈ div_hide P A},
 div_hide P A)›
proof - 
  show ‹?thesis P A› (is ‹is_process(?f, div_hide P A)›) for P and A
  proof (unfold is_process_def FAILURES_def DIVERGENCES_def fst_conv snd_conv, intro conjI allI impI)
    from inf_hidden[of A ‹[]› P] show ‹([], {}) ∈ ?f›
      by simp (metis filter.simps(1) tickFree_Nil)
  next
    show ‹(s, X) ∈ ?f ==> ftF s› for s X
      by simp (metis F_imp_front_tickFree Hiding_front_tickFree Hiding_tickFree 
          front_tickFree_append_iff tickFree_imp_front_tickFree)
  next
    show ‹(s @ t, {}) ∈ ?f ==> (s, {}) ∈ ?f› for s t
    proof (induct t rule: rev_induct)
      case Nil
      then show ?case by auto
    next
      case (snoc e t)
      from snoc.prems consider u where ‹s @ t @ [e] = trace_hide u (ev ` A)› ‹(u, ev ` A) ∈ F P›
        | u v where ‹ftF v› ‹tF u› ‹s @ t @ [e] = trace_hide u (ev ` A) @ v›
          ‹u ∈ D P ∨ (∃f. isInfHiddenRun f P A ∧ u ∈ range f)›
        by simp blast
      thus ?case
      proof cases
        fix u assume ‹s @ t @ [e] = trace_hide u (ev ` A)› ‹(u, ev ` A) ∈ F P›
        from this(1) obtain u' u'' where ‹u = u' @ u''› ‹s @ t = trace_hide u' (ev ` A)›
          by (metis append_assoc trace_hide_append)
        have ‹(s @ t, {}) ∈ ?f›
        proof (cases ‹∃t. trace_hide t (ev ` A) = trace_hide u' (ev ` A) ∧ (t, ev ` A) ∈ F P›)
          show ‹∃t. trace_hide t (ev ` A) = trace_hide u' (ev ` A) ∧ (t, ev ` A) ∈ F P ==>
 (s @ t, {}) ∈ ?f›
            by (simp add: ‹s @ t = trace_hide u' (ev ` A)›) metis
        next
          assume * : ‹∄t. trace_hide t (ev ` A) = trace_hide u' (ev ` A) ∧ (t, ev ` A) ∈ F P›
          from this[simplified, THEN inf_hidden] obtain f where ‹isInfHiddenRun f P A ∧ u' ∈ range f›
            using T_F_spec ‹(u, ev ` A) ∈ F P› ‹u = u' @ u''› is_processT3 is_processT4_empty by blast
          hence ‹s @ t ∈ div_hide P A›
            by (simp add: ‹s @ t = trace_hide u' (ev ` A)›) 
              (metis F_imp_front_tickFree ‹(u, ev ` A) ∈ F P› "*" ‹u = u' @ u''›
                append.right_neutral front_tickFree_Nil front_tickFree_append_iff)
          thus ‹(s @ t, {}) ∈ ?f› by simp
        qed
        from snoc.hyps[OF this] show ‹(s, {}) ∈ ?f› by blast
      next
        fix u v assume * : ‹ftF v› ‹tF u› ‹s @ t @ [e] = trace_hide u (ev ` A) @ v›
          ‹u ∈ D P ∨ (∃f. isInfHiddenRun f P A ∧ u ∈ range f)›
        show ?case
        proof (cases v rule: rev_cases)
          assume ‹v = []›
          with "*"(3) obtain u' u'' where ‹u = u' @ u''› ‹s @ t = trace_hide u' (ev ` A)›
            by simp (metis append_assoc trace_hide_append)
          from "*"(4) D_T have ‹u ∈ T P› by blast
          have ‹(s @ t, {}) ∈ ?f›
          proof (cases ‹∃t. trace_hide t (ev ` A) = trace_hide u' (ev ` A) ∧ (t, ev ` A) ∈ F P›)
            show ‹∃t. trace_hide t (ev ` A) = trace_hide u' (ev ` A) ∧ (t, ev ` A) ∈ F P ==>
 (s @ t, {}) ∈ ?f›
              by (simp add: ‹s @ t = trace_hide u' (ev ` A)›) metis
          next
            assume * : ‹∄t. trace_hide t (ev ` A) = trace_hide u' (ev ` A) ∧ (t, ev ` A) ∈ F P›
            from this[simplified, THEN inf_hidden] obtain f where ‹isInfHiddenRun f P A ∧ u' ∈ range f›
              by (metis T_F_spec ‹u = u' @ u''› ‹u ∈ T P› is_processT3)
            hence ‹s @ t ∈ div_hide P A›
              by (simp add: ‹s @ t = trace_hide u' (ev ` A)›) 
                (metis (no_types, lifting) "*" append_Nil2 append_T_imp_tickFree
                  front_tickFree_Nil is_processT5_S7 list.distinct(1) rangeE)
            thus ‹(s @ t, {}) ∈ ?f› by simp
          qed
          from snoc.hyps[OF this] show ‹(s, {}) ∈ ?f› by blast
        next
          fix v' e'
          assume ‹v = v' @ [e']›
          with "*" front_tickFree_dw_closed have ‹s @ t ∈ div_hide P A› by auto
          hence ‹(s @ t, {}) ∈ ?f› by simp
          from snoc.hyps[OF this] show ‹(s, {}) ∈ ?f› by blast
        qed
      qed
    qed

  next
    show $ : ‹(s, Y) ∈ ?f ∧ X ⊆ Y ==> (s, X) ∈ ?f› for s X Y
      by simp (metis is_processT4 subset_iff_psubset_eq sup.mono)
  next
    fix s X Y assume * : ‹(s, X) ∈ ?f ∧ (∀c. c ∈ Y ⟶ (s @ [c], {}) ∉ ?f)›
    from "*"[THEN conjunct1] consider ‹s ∈ div_hide P A›
      | u where ‹s = trace_hide u (ev ` A)› ‹(u, X ∪ ev ` A) ∈ F P› by simp blast
    thus ‹(s, X ∪ Y) ∈ ?f›
    proof cases
      show ‹s ∈ div_hide P A ==> (s, X ∪ Y) ∈ ?f› by simp
    next
      fix u assume ‹s = trace_hide u (ev ` A)› ‹(u, X ∪ ev ` A) ∈ F P›
      show ‹(s, X ∪ Y) ∈ ?f›
      proof (cases ‹s ∈ div_hide P A›)
        show ‹s ∈ div_hide P A ==> (s, X ∪ Y) ∈ ?f› by simp
      next
        assume ‹s ∉ div_hide P A›  
        have ‹(u, X ∪ Y ∪ ev ` A) ∈ F P›
        proof (rule ccontr)
          assume ‹(u, X ∪ Y ∪ ev ` A) ∉ F P›
          hence ‹(u, X ∪ ev ` A ∪ Y) ∉ F P› by (metis sup.assoc sup_commute)
          from is_processT5_S7'[OF ‹(u, X ∪ ev ` A) ∈ F P› this] obtain c
            where ‹c ∈ Y› ‹c ∉ X› ‹c ∉ ev ` A› ‹u @ [c] ∈ T P› by blast
          show False
          proof (cases ‹∃t. trace_hide t (ev ` A) = trace_hide (u @ [c]) (ev ` A) ∧ (t, ev ` A) ∈ F P›)
            show ‹∃t. trace_hide t (ev ` A) = trace_hide (u @ [c]) (ev ` A) ∧ (t, ev ` A) ∈ F P ==> False›
              using "*" ‹c ∈ Y› ‹c ∉ ev ` A› ‹s = trace_hide u (ev ` A)› by force
          next
            assume ‹∄t. trace_hide t (ev ` A) = trace_hide (u @ [c]) (ev ` A) ∧ (t, ev ` A) ∈ F P›
            hence ‹∀t. trace_hide t (ev ` A) = trace_hide (u @ [c]) (ev ` A)
 ⟶ (t, ev ` A) ∉ F P› by simp
            from inf_hidden[OF this ‹u @ [c] ∈ T P›] have ‹s @ [c] ∈ div_hide P A›
              (* TODO : break this smt *)
              by (smt (verit, ccfv_threshold) Prefix_Order.strict_prefix_simps(1)
                  Prefix_Order.strict_prefix_simps(2)
                  ‹∄t. trace_hide t (ev ` A) = trace_hide (u @ [c]) (ev ` A) ∧ (t, ev ` A) ∈ F P›
                  ‹s = trace_hide u (ev ` A)› ‹s ∉ div_hide P A› ‹u @ [c] ∈ T P› append_Nil2
                  append_T_imp_tickFree filter.simps(1) filter.simps(2) filter_append
                  front_tickFree_Nil is_processT5_S7 mem_Collect_eq)
            thus False using "*" ‹c ∈ Y› by blast
          qed
        qed
        thus ‹(s, X ∪ Y) ∈ ?f› by (auto simp add: ‹s = trace_hide u (ev ` A)›)
      qed
    qed
  next
    { fix s r assume ‹s @ [🍋(r)] ∈ div_hide P A›
      then obtain t u where * : ‹ftF u› ‹tF t›
        ‹s @ [🍋(r)] = trace_hide t (ev ` A) @ u›
        ‹t ∈ D P ∨ (∃f. isInfHiddenRun f P A ∧ t ∈ range f)› by blast
      from "*"(2, 3) have ‹u ≠ []›
        by (cases u; cases t rule: rev_cases; simp split: if_split_asm)
          (metis Hiding_tickFree non_tickFree_tick tickFree_append_iff)
      with "*"(2, 3) have ‹s = trace_hide t (ev ` A) @ butlast u›
        by (cases u rule: rev_cases; simp)
      moreover from "*"(1)front_tickFree_iff_tickFree_butlast tickFree_imp_front_tickFree
      have ‹ftF (butlast u)› by blast
      ultimately show ‹s ∈ div_hide P A› using "*"(2, 4) by auto
    } note local_is_processT9 = this

    fix s r X assume ‹(s @ [🍋(r)], {}) ∈ ?f›
    then consider ‹s @ [🍋(r)] ∈ div_hide P A›
      | u where ‹s @ [🍋(r)] = trace_hide u (ev ` A)› ‹(u, ev ` A) ∈ F P› by simp blast
    thus ‹(s, X - {tick r}) ∈ ?f›
    proof cases
      assume ‹s @ [🍋(r)] ∈ div_hide P A›
      with local_is_processT9 have ‹s ∈ div_hide P A› by blast
      thus ‹(s, X - {tick r}) ∈ ?f› by simp
    next
      fix u assume ‹s @ [🍋(r)] = trace_hide u (ev ` A)› ‹(u, ev ` A) ∈ F P›
      from this(1) obtain u' where ‹u = u' @ [🍋(r)]› ‹s = trace_hide u' (ev ` A)›
        by (cases u rule: rev_cases; simp split: if_split_asm)
          (metis F_imp_front_tickFree Hiding_tickFree ‹(u, ev ` A) ∈ F P› tickFree_append_iff
            front_tickFree_iff_tickFree_butlast non_tickFree_tick snoc_eq_iff_butlast)
      have ‹X - {🍋(r)} ∪ ev ` A = X ∪ ev ` A - {🍋(r)}› by auto
      with is_processT6_TR[OF ‹(u, ev ` A) ∈ F P›[THEN F_T, unfolded ‹u = u' @ [🍋(r)]›]]
      have ‹(u', X - {🍋(r)} ∪ ev ` A) ∈ F P› by presburger
      thus ‹(s, X - {tick r}) ∈ ?f› by (auto simp add: ‹s = trace_hide u' (ev ` A)›)
    qed
  next
    fix s t :: ‹('a, 'r) trace<sub>ptick</sub>› assume * : ‹s ∈ div_hide P A ∧ tF s ∧ ftF t›
    from "*"[THEN conjunct1] obtain u v
      where ** : ‹ftF v› ‹tF u› ‹s = trace_hide u (ev ` A) @ v›
        ‹u ∈ D P ∨ (∃f. isInfHiddenRun f P A ∧ u ∈ range f)› by blast
    from "**"(3) have ‹s @ t = trace_hide u (ev ` A) @ v @ t› by simp
    moreover from "*" "**"(3) front_tickFree_append have ‹ftF (v @ t)› by auto
    ultimately show ‹s @ t ∈ div_hide P A› using "**"(2) "**"(4) by blast
  next
    show ‹s ∈ div_hide P A ==> (s, X) ∈ ?f› for s X by simp
  qed
qed



section‹Projections›

lemma F_Hiding: ‹F (P \ A) = {(s, X). ∃t. s = trace_hide t (ev ` A) ∧ (t, X ∪ ev ` A) ∈ F P} ∪
 {(s, X). s ∈ div_hide P A}›
  by (simp add: Failures.rep_eq Hiding.rep_eq FAILURES_def)

lemma D_Hiding: ‹D (P \ A) = div_hide P A›
  by (simp add: Divergences.rep_eq Hiding.rep_eq DIVERGENCES_def)

lemma T_Hiding: ‹T (P \ A) = {trace_hide t (ev ` A) |t. (t, ev ` A) ∈ F P} ∪ div_hide P A›
  by (auto simp add: Traces.rep_eq TRACES_def Failures.rep_eq[symmetric] F_Hiding)
    (metis is_processT4 sup_ge2, metis sup_bot_left)

lemma Hiding_empty: ‹P \ {} = P›
  by (auto simp add: Process_eq_spec D_Hiding F_Hiding strict_mono_eq
      intro: is_processT7 is_processT8)
    (metis append.right_neutral front_tickFree_append_iff
      list.distinct(1) nonTickFree_n_frontTickFree process_charn)


lemma mem_D_imp_mem_D_Hiding: ‹trace_hide t (ev ` A) ∈ D (P \ A)› if ‹t ∈ D P›
proof (cases ‹tF t›)
  assume ‹tF t›
  with ‹t ∈ D P› show ‹trace_hide t (ev ` A) ∈ D (P \ A)›
    by (simp add: D_Hiding) (use front_tickFree_Nil in blast)
next
  assume ‹¬ tF t›
  with ‹t ∈ D P› obtain t' r where ‹t = t' @ [🍋(r)]› ‹tF t'› ‹t' ∈ D P›
    by (metis D_imp_front_tickFree butlast_snoc is_processT9
        front_tickFree_iff_tickFree_butlast nonTickFree_n_frontTickFree)
  thus ‹trace_hide t (ev ` A) ∈ D (P \ A)›
    by (simp add: D_Hiding) (use front_tickFree_single in blast)
qed

lemma mem_T_imp_mem_T_Hiding: ‹trace_hide t (ev ` A) ∈ T (P \ A)› if ‹t ∈ T P›
proof (cases ‹∃t'. trace_hide t (ev ` A) = trace_hide t' (ev ` A) ∧ (t', ev ` A) ∈ F P›)
  show ‹∃t'. trace_hide t (ev ` A) = trace_hide t' (ev ` A) ∧ (t', ev ` A) ∈ F P
 ==> trace_hide t (ev ` A) ∈ T (P \ A)› by (simp add: T_Hiding)
next
  assume ‹∄t'. trace_hide t (ev ` A) = trace_hide t' (ev ` A) ∧ (t', ev ` A) ∈ F P›
  with inf_hidden[of A, OF _ ‹t ∈ T P›] obtain f
    where ‹isInfHiddenRun f P A› ‹t ∈ range f› ‹tF t›
    by (metis T_nonTickFree_imp_decomp ‹t ∈ T P› tick_T_F)
  thus ‹trace_hide t (ev ` A) ∈ T (P \ A)›
    by (simp add: T_Hiding) (use front_tickFree_Nil in blast)
qed



section‹Continuity Rule›

lemma mono_Hiding : ‹(P \ A) ⊑ (Q \ A)› if ‹(P::('a, 'r) process_ptick) ⊑ Q›
proof (unfold le_approx_def, intro conjI allI impI subsetI)
  from le_approx1[OF ‹P ⊑ Q›] le_approx_lemma_T[OF ‹P ⊑ Q›]
  show ‹s ∈ D (Q \ A) ==> s ∈ D (P \ A)› for s
    by (simp add: D_Hiding) blast
next
  { fix s t X
    assume assms : ‹s ∉ D (P \ A)› ‹s = trace_hide t (ev ` A)›
    have ‹t ∉ D P›
    proof (cases ‹ftF t›)
      from D_imp_front_tickFree show ‹¬ ftF t ==> t ∉ D P› by blast
    next
      assume ‹ftF t›
      show ‹t ∉ D P›
      proof (cases ‹tF t›)
        from ‹s ∉ D (P \ A)› show ‹tF t ==> t ∉ D P›
          by (simp add: assms(2) D_Hiding)
      next
        assume ‹¬ tF t›
        then obtain t' r where ‹t = t' @ [tick r]›
          by (meson ‹ftF t› nonTickFree_n_frontTickFree process_charn)
        with ‹s ∉ D (P \ A)› show ‹t ∉ D P›
          by (simp add: assms(2) D_Hiding image_iff)
            (metis front_tickFree_append_iff list.distinct(1) process_charn)
      qed
    qed
  } note * = this

  fix s
  assume ‹s ∉ D (P \ A)›
  show ‹R_a (P \ A) s = R_a (Q \ A) s›
  proof (intro subset_antisym subsetI)
    fix X
    assume ‹X ∈ R_a (P \ A) s›
    with le_approx1[OF ‹P ⊑ Q›] le_approx_lemma_T[OF ‹P ⊑ Q›] ‹s ∉ D (P \ A)›
    obtain t where $ : ‹s = trace_hide t (ev ` A)› ‹(t, X ∪ ev ` A) ∈ F P›
      by (simp add: Refusals_after_def F_Hiding D_Hiding) blast
    from "*"[OF ‹s ∉ D (P \ A)› ‹s = trace_hide t (ev ` A)›] have ‹t ∉ D P› .
    from le_approx2[OF ‹P ⊑ Q› this] "$"
    show ‹X ∈ R<sub>a</sub> (Q \ A) s› by (simp add: Refusals_after_def F_Hiding) blast
  next
    fix X
    assume ‹X ∈ R<sub>a</sub> (Q \ A) s›
    with le_approx1[OF ‹P ⊑ Q›] le_approx_lemma_T[OF ‹P ⊑ Q›] ‹s ∉ D (P \ A)›
    obtain t where $ : ‹s = trace_hide t (ev ` A)› ‹(t, X ∪ ev ` A) ∈ F Q›
      by (simp add: Refusals_after_def F_Hiding D_Hiding) blast
    from "*"[OF ‹s ∉ D (P \ A)› ‹s = trace_hide t (ev ` A)›] have ‹t ∉ D P› .
    from le_approx2[OF ‹P ⊑ Q› this] "$"
    show ‹X ∈ R_a (P \ A) s› by (simp add: Refusals_after_def F_Hiding) blast
  qed
next
  fix s
  assume ‹s ∈ min_elems (D (P \ A))›

  { fix t 
    assume assms : ‹t ∈ D P› ‹s = trace_hide t (ev ` A)› ‹tF t›
    from assms(1) obtain t' t'' where ‹t = t' @ t''› and ‹t' ∈ min_elems (D P)›
      by (meson min_elems_charn)
    with assms(3) elem_min_elems tickFree_append_iff
    have ‹trace_hide t' (ev ` A) ∈ D (P \ A)›
      by (simp add: D_Hiding) (use front_tickFree_Nil in blast)
    from filter_append[of ‹(λx. x ∉ ev ` A)› t' t'', folded ‹t = t' @ t''›]
    have ‹trace_hide t (ev ` A) = trace_hide t' (ev ` A) @ trace_hide t'' (ev ` A)› .
    hence ‹s = trace_hide t' (ev ` A)›
      by (metis (no_types, lifting) assms(2) ‹s ∈ min_elems (D (P \ A))›
          min_elems_no ‹trace_hide t' (ev ` A) ∈ D (P \ A)› less_eq_list_def prefix_def)
    have ‹s ∈ T (Q \ A)›
    proof (cases ‹∀v. trace_hide v (ev ` A) = trace_hide t' (ev ` A) ⟶ (v, ev ` A) ∉ F Q›)
      assume ‹∀v. trace_hide v (ev ` A) = trace_hide t' (ev ` A) ⟶ (v, ev ` A) ∉ F Q›
      from inf_hidden[OF this] have ‹∃f. isInfHiddenRun f Q A ∧ t' ∈ range f›
        by (meson ‹t' ∈ min_elems (D P)› in_mono le_approx_def that)
      thus ‹s ∈ T (Q \ A)›
        by (simp add: T_Hiding)
          (use assms(3) ‹s = trace_hide t' (ev ` A)› ‹t = t' @ t''›
            front_tickFree_Nil tickFree_append_iff in blast)
    next
      show ‹¬ (∀v. trace_hide v (ev ` A) = trace_hide t' (ev ` A)
 ⟶ (v, ev ` A) ∉ F Q) ==> s ∈ T (Q \ A)›
        by (simp add: T_Hiding) (metis ‹s = trace_hide t' (ev ` A)›)
    qed
  } note $ = this

  from elem_min_elems[OF ‹s ∈ min_elems (D (P \ A))›] have ‹s ∈ D (P \ A)› .
  then obtain t u
    where * : ‹ftF u› ‹tF t› ‹s = trace_hide t (ev ` A) @ u›
      ‹t ∈ D P ∨ (∃f. isInfHiddenRun f P A ∧ t ∈ range f)›
    by (simp add: D_Hiding) blast
  have ‹u = []›
  proof (rule ccontr)
    assume ‹u ≠ []›
    have ‹ftF (butlast u)› ‹butlast s = trace_hide t (ev ` A) @ butlast u›
      by (use "*"(1) front_tickFree_iff_tickFree_butlast tickFree_imp_front_tickFree in blast)
        (simp add: "*"(3) ‹u ≠ []› butlast_append)
    with "*"(2, 4) have ‹butlast s ∈ D (P \ A)› by (simp add: D_Hiding) blast
    from min_elems_no[OF ‹s ∈ min_elems (D (P \ A))› this] "*"(3) ‹u ≠ []›
    show False by (metis Nil_is_append_conv append_butlast_last_id less_self nless_le)
  qed

  from "*"(4) show ‹s ∈ T (Q \ A)›
  proof (elim disjE exE)
    show ‹t ∈ D P ==> s ∈ T (Q \ A)› using "$" "*"(2, 3) ‹u = []› by blast
  next
    fix f
    assume assm : ‹isInfHiddenRun f P A ∧ t ∈ range f›
    show ‹s ∈ T (Q \ A)›
    proof (cases ‹∀i. f i ∈ T Q›)
      from "*"(1, 2, 3) assm show ‹∀i. f i ∈ T Q ==> s ∈ T (Q \ A)›
        by (simp add: T_Hiding) blast
    next
      assume ‹¬ (∀i. f i ∈ T Q)›
      then obtain i where ‹f i ∉ T Q›  by blast
      with assm le_approx2T ‹P ⊑ Q› have ‹f i ∈ D P› by blast
      moreover have ‹s = trace_hide (f i) (ev ` A)›
        by (metis "*"(3) ‹u = []› append.right_neutral assm rangeE)
      moreover have ‹tF (f i)›
        by (metis "*"(2) "*"(3) Hiding_tickFree ‹u = []› append.right_neutral calculation(2))
      ultimately show ‹s ∈ T (Q \ A)› using "$" by blast
    qed
  qed
qed


lemma chain_Hiding : ‹chain Y ==> chain (λ i. Y i \ A)›
  by (simp add: chain_def mono_Hiding)

lemma KoenigLemma: 
  ‹∃(f::nat ==> 'a list). strict_mono f ∧ range f ⊆ {t. ∃t'∈Tr. t ≤ t'}›
  if * : ‹infinite (Tr::'a list set)› and ** : ‹∀i. finite{t. ∃t'∈Tr. t = take i t'}›
proof -
  define Tr' where ‹Tr' = {t. ∃t'∈Tr. t ≤ t'}› (* prefix closure *)
  have a : ‹infinite Tr'› by (rule infinite_super[OF _ "*"]) (unfold Tr'_def, blast)
  have b : ‹finite {t ∈ Tr'. length t = i}› for i
    by (rule finite_subset[OF _ "**"[THEN spec, of i]])
      (unfold Tr'_def, simp add: subset_iff, metis prefixE append_eq_conv_conj)
  have c : ‹∃e. infinite {t' ∈ Tr'. t @ [e] < t'}› if ‹infinite {t' ∈ Tr'. t < t'}› for t
  proof (rule ccontr)
    assume ‹∄e. infinite {t' ∈ Tr'. t @ [e] < t'}›
    define E where ‹E ≡ {e |e. t @ [e] ∈ Tr'}›
    have ‹finite E›
      by (rule inj_on_finite[OF _ _ b[of ‹Suc (length t)›], of ‹λe. t @ [e]›])
        (simp_all add: inj_on_def E_def image_Collect_subsetI)
    hence ‹finite {t @ [e] |e. e ∈ E}› by simp
    have ‹{t' ∈ Tr'. t < t'} = {t @ [e] |e. e ∈ E} ∪ (∪e∈E. {t' ∈ Tr'. t @ [e] < t'})›
      by (auto simp add: E_def Tr'_def less_list_def less_eq_list_def prefix_def)+
        (metis append_Cons append_self_conv2 neq_Nil_conv self_append_conv)
    with ‹∄e. infinite {t' ∈ Tr'. t @ [e] < t'}› ‹infinite {t' ∈ Tr'. t < t'}› ‹finite E›
    show False by auto
  qed

  define f where ‹f ≡ rec_nat [] (λi t. let e = SOME e. infinite {t' ∈ Tr'. t @ [e] < t'} in t @ [e])›
  hence ‹strict_mono f› by (simp add: lift_Suc_mono_less strict_monoI)
  moreover have ‹f n ∈ Tr' ∧ infinite {t' ∈ Tr'. f n < t'}› for n
  proof (induct n)
    show ‹f 0 ∈ Tr' ∧ infinite {t' ∈ Tr'. f 0 < t'}›
    proof (rule conjI)
      show ‹f 0 ∈ Tr'› by (simp add: f_def Tr'_def "*" not_finite_existsD)
    next
      show ‹infinite {t' ∈ Tr'. f 0 < t'}›
        by (rule infinite_super[of ‹Tr' - {f 0}›])
          (simp add: a Tr'_def f_def subset_iff less_list_def, simp add: a)
    qed
  next
    fix n assume hyp : ‹f n ∈ Tr' ∧ infinite {t' ∈ Tr'. f n < t'}›
    have ‹f (Suc n) = (let e = SOME e. infinite {t' ∈ Tr'. f n @ [e] < t'} in f n @ [e])›
      by (simp add: f_def)
    with c[of ‹f n›] obtain e
      where $ : ‹f (Suc n) = f n @ [e] ∧ infinite {t' ∈ Tr'. f n @ [e] < t'}›
      by (metis (no_types, lifting) hyp someI_ex)
    then obtain i where ‹i ∈ Tr' ∧ f (Suc n) < i› using not_finite_existsD by auto 
    with dual_order.trans order_less_imp_le have ‹f (Suc n) ∈ Tr'›
      unfolding Tr'_def by fastforce
    thus ‹f (Suc n) ∈ Tr' ∧ infinite {t' ∈ Tr'. f (Suc n) < t'}› by (simp add: "$")
  qed
  ultimately show ‹∃(f::nat ==> 'a list). strict_mono f ∧ range f ⊆ Tr'› by blast
qed

(* 
lemma isInfHiddenRun_chain :
 \<open>chain Y \<Longrightarrow> isInfHiddenRun f (Y (Suc i)) A \<Longrightarrow> isInfHiddenRun f (Y i) A\<close>
  using D_T le_approx2T chain_def by blast
 *)


(* TODO: redo this proof properly *)
lemma div_Hiding_lub :  
  ‹finite (A::'a set) ==> chain Y ==> D (⊔ i. (Y i \ A)) ⊆ D ((⊔ i. Y i) \ A)›
  for Y :: ‹nat ==> ('a, 'r) process_ptick›
proof (auto simp add:limproc_is_thelub chain_Hiding D_Hiding T_Hiding D_LUB T_LUB, goal_cases)
  case (1 x)
  { fix xa t u f
    assume a:"ftF u ∧ tF t ∧ x = trace_hide t (ev ` A) @ u ∧
              isInfHiddenRun f (Y xa) A ∧ (∀ i. f i ∉ D (Y xa)) ∧ t ∈ range f"
    hence "∀i n. f i ∈ T (Y n)" using "1"(2) D_T chain_lemma le_approx2T by blast
    with a have ?case by blast
  } note aa=this 
  { fix xa t u f j
    assume a:"ftF u ∧ tF t ∧ x = trace_hide t (ev ` A) @ u ∧
              isInfHiddenRun f (Y xa) A ∧ (f j ∈ D (Y xa)) ∧ t ∈ range f"
    hence "∃t u. ftF u ∧ tF t ∧ x = trace_hide t (ev ` A) @ u ∧ t ∈ D (Y xa)"
      apply(rule_tac x="f j" in exI, rule_tac x=u in exI) 
      by (metis Hiding_tickFree rangeE)
  } note bb=this
  have cc: "∀xa. ∃t u. ftF u ∧ tF t ∧ x = trace_hide t (ev ` A) @ u ∧ t ∈ D(Y xa)
           ==> ?case" (is "∀xa. ∃t. ?S t xa ==> ?case")
  proof -
    assume dd:"∀xa. ∃t u. ftF u ∧ tF t ∧ x = trace_hide t (ev ` A) @ u ∧ t ∈ D(Y xa)"
      (is "∀xa. ∃t. ?S t xa")
    define f :: ‹nat ==> ('a, 'r) event<sub>ptick</sub> list› where "f = (λn. SOME t. ?S t n)"
    thus ?case 
    proof (cases "finite(range f)")
      case True
      obtain t where gg:"infinite (f -` {t})" using f_def True inf_img_fin_dom by blast 
      then obtain k where "f k = t" using finite_nat_set_iff_bounded_le by blast
      then obtain u where uu:"ftF u ∧ x = trace_hide t (ev ` A) @ u ∧ tF t"
        using f_def dd[rule_format, of k] some_eq_ex[of "λt. ?S t k"] by blast
      { fix m
        from gg obtain n where gg:"n ≥ m ∧ n ∈ (f -` {t})"
          by (meson finite_nat_set_iff_bounded_le nat_le_linear)
        hence "t ∈ D (Y n)" using f_def dd[rule_format, of n] some_eq_ex[of "λt. ?S t n"] by auto
        with gg 1(2) have "t ∈ D (Y m)" by (meson contra_subsetD le_approx_def po_class.chain_mono)
      }
      with gg uu show ?thesis by blast
    next
      case False
      { fix t
        assume "t ∈ range f"
        then obtain k where "f k = t" using finite_nat_set_iff_bounded_le by blast
        then obtain u where uu:"ftF u ∧ x = trace_hide t (ev ` A) @ u ∧ tF t"
          using f_def dd[rule_format, of k] some_eq_ex[of "λt. ?S t k"] by blast
        hence "set t ⊆ set x ∪ (ev ` A)" by auto
      } note ee=this
      { fix i
        have "finite {(take i t)|t. t ∈ range f}" 
        proof(induct i, simp)
          case (Suc i)
          have ff:"{take (Suc i) t|t. t ∈ range f} ⊆ {(take i t)|t. t ∈ range f} ∪
                        (∪e∈(set x ∪ (ev ` A)). {(take i t)@[e]|t. t ∈ range f})" (is "?AA ⊆ ?BB")
          proof
            fix t
            assume "t ∈ ?AA"
            then obtain t' where hh:"t' ∈ range f ∧ t = take (Suc i) t'" 
              using finite_nat_set_iff_bounded_le by blast
            with ee[of t'] show "t ∈ ?BB"
            proof(cases "length t' > i")
              case True
              hence ii:"take (Suc i) t' = take i t' @ [t'!i]" by (simp add: take_Suc_conv_app_nth)
              with ee[of t'] have "t'!i ∈ set x ∪ (ev ` A)" 
                by (meson True contra_subsetD hh nth_mem)
              with ii hh show ?thesis by blast
            next
              case False
              hence "take (Suc i) t' = take i t'" by fastforce
              with hh show ?thesis by auto
            qed
          qed
          { fix e 
            have "{x @ [e] |x. ∃t. x = take i t ∧ t ∈ range f} = {take i t' @ [e] |t'. t' ∈ range f}"
              by auto
            hence "finite({(take i t') @ [e] |t'. t'∈range f})"
              using finite_image_set[of _ "λt. t@[e]", OF Suc] by auto 
          } note gg=this
          have "finite(set x ∪ (ev ` A))" using 1(1) by simp
          with ff gg Suc show ?case by (metis (no_types, lifting) finite_UN finite_Un finite_subset)
        qed
      } note ff=this
      hence "∀i. {take i t |t. t ∈ range f} = {t. ∃t'. t = take i (f t')}" by auto
      with KoenigLemma[of "range f", OF False] ff
      obtain f' where gg:"strict_mono (f':: nat ==> ('a, 'r) event<sub>ptick</sub> list) ∧
                                            range f' ⊆ {t. ∃t'∈range f. t ≤ t'}" by auto
      { fix n
        define M where "M = {m. f' n ≤ f m }"
        assume "finite M"
        hence l1:"finite {length (f m)|m. m ∈ M}" by simp
        obtain lm where l2:"lm = Max {length (f m)|m. m ∈ M}" by blast
        { fix k
          have "length (f' k) ≥ k" 
            by(induct k, simp, metis (full_types) gg lessI less_length_mono linorder_not_le 
                not_less_eq_eq order_trans strict_mono_def)
        }
        with gg obtain m where r1:"length (f' m) > lm" by (meson lessI less_le_trans)
        from gg obtain r where r2:"f' (max m n) ≤ f r" by blast
        with gg have r3: "r ∈ M" 
          by (metis (no_types, lifting) M_def max.bounded_iff mem_Collect_eq order_refl 
              order_trans strict_mono_less_eq)
        with l1 l2 have f1:"length (f r) ≤ lm" using Max_ge by blast
        from r1 r2 have f2:"length (f r) > lm"
          by (meson dual_order.strict_trans1 gg le_length_mono max.bounded_iff order_refl 
              strict_mono_less_eq) 
        from f1 f2 have False by simp
      } note ii=this
      { fix i n
        from ii obtain m where jj:"m ≥ n ∧ f m ≥ f' i" 
          by (metis finite_nat_set_iff_bounded_le mem_Collect_eq nat_le_linear)
        have kk: "(f m) ∈ D (Y m)" using f_def dd[rule_format, of m] some_eq_ex[of "λt. ?S t m"] by auto 
        with jj gg have "(f' i) ∈ T (Y m)" by (meson D_T is_processT3_TR)
        with jj 1(2) have  "(f' i) ∈ T (Y n)" using D_T le_approx2T po_class.chain_mono by blast
      } note jj=this
      from gg have kk:"mono (λn. trace_hide (f' n) (ev ` A))" 
        unfolding strict_mono_def mono_def
        by (metis (no_types, lifting) filter_append gg less_eq_list_def prefix_def mono_def strict_mono_mono)
      { fix n
        from gg obtain k r where "f k = f' n @ r"
          by (metis (lifting) ii less_eq_list_def prefix_def not_finite_existsD)
        hence "trace_hide (f' n) (ev ` A) ≤ x" 
          using f_def dd[rule_format, of k] some_eq_ex[of "λt. ?S t k"]
          by (metis (no_types, lifting) prefixI prefix_prefix filter_append)
      } note ll=this
      { assume llll:"∀m. ∃n. trace_hide (f' n) (ev ` A) > trace_hide (f' m) (ev ` A)"
        hence lll:"∀m. ∃n. length (trace_hide (f' n) (ev ` A)) > length (trace_hide (f' m) (ev ` A))"
          using less_length_mono by blast
        define ff where lll':"ff = rec_nat (length (trace_hide (f' 0) (ev ` A)))
                (λi t. (let n = SOME n. (length (trace_hide (f' n) (ev ` A))) > t
                         in length (trace_hide (f' n) (ev ` A))))"
        { fix n
          from lll' lll[rule_format, of n] have "ff (Suc n) > ff n" 
            apply simp apply (cases n)
             apply (metis (no_types, lifting) old.nat.simps(6) someI_ex)
            by (metis (no_types, lifting) llll less_length_mono old.nat.simps(7) someI_ex)
        } note lll''=this
        with lll'' have "strict_mono ff" by (simp add: lll'' lift_Suc_mono_less strict_monoI)
        hence lll''':"infinite(range ff)" using finite_imageD strict_mono_imp_inj_on by auto
        from lll lll' have "range ff ⊆ range (λn. length (trace_hide (f' n) (ev ` A)))" 
          by (auto, metis (mono_tags, lifting) old.nat.exhaust old.nat.simps(6) old.nat.simps(7) range_eqI)
        with lll''' have "infinite (range (λn. length (trace_hide (f' n) (ev ` A))))"
          using finite_subset by auto
        hence "∃m. length (trace_hide (f' m) (ev ` A)) > length x"
          using finite_nat_set_iff_bounded_le by (metis (no_types, lifting) not_less rangeE)
        with ll have False using le_length_mono not_less by blast
      }
      then obtain m where mm:"∀n. trace_hide (f' n) (ev ` A) ≤ trace_hide (f' m) (ev ` A)"
        by (metis (no_types, lifting) dual_order.eq_iff le_same_imp_eq_or_less ll order.strict_implies_order)
      with gg obtain k where nn:"f k ≥ f' m" by blast
      then obtain u where oo:"ftF u ∧ x = trace_hide (f' m) (ev ` A) @ u ∧ tF (f' m)"
        using f_def dd[rule_format, of k] some_eq_ex[of "λt. ?S t k"] 

        apply (auto simp add: prefix_def tickFree_def disjoint_iff)
        by (smt (z3) Prefix_Order.prefixE append.assoc disjoint_iff filter_append filter_is_subset front_tickFree_append subset_iff tickFree_append_iff tickFree_def)
          (*  proof -
          fix t :: "('a, 'r) event\<^sub>p\<^sub>t\<^sub>i\<^sub>c\<^sub>k list" and u :: "('a, 'r) event\<^sub>p\<^sub>t\<^sub>i\<^sub>c\<^sub>k list" and ua :: "('a, 'r) event\<^sub>p\<^sub>t\<^sub>i\<^sub>c\<^sub>k list"
          assume a1: "\<forall>x. x \<in> range tick \<longrightarrow> x \<notin> set (SOME x. \<exists>u. ftF u \<and> (\<forall>xa. xa \<in> range tick \<longrightarrow> xa \<notin> set x) \<and> trace_hide t (ev ` A) @ ua = trace_hide x (ev ` A) @ u \<and> x \<in> \<D> (Y k))"
          assume a2: "\<And>u. ftF u \<and> trace_hide t (ev ` A) @ ua = trace_hide (f' m) (ev ` A) @ u \<and> (\<forall>x. x \<in> range tick \<longrightarrow> x \<notin> set (f' m)) \<Longrightarrow> thesis"
          assume a3: "trace_hide t (ev ` A) @ ua = trace_hide (SOME x. \<exists>u. ftF u \<and> (\<forall>xa. xa \<in> range tick \<longrightarrow> xa \<notin> set x) \<and> trace_hide t (ev ` A) @ ua = trace_hide x (ev ` A) @ u \<and> x \<in> \<D> (Y k)) (ev ` A) @ u"
          assume a4: "f' m \<le> (SOME ta. \<exists>u. ftF u \<and> (\<forall>x. x \<in> range tick \<longrightarrow> x \<notin> set ta) \<and> trace_hide t (ev ` A) @ ua = trace_hide ta (ev ` A) @ u \<and> ta \<in> \<D> (Y k))"
          assume a5: "ftF u"
          obtain ee :: "('a, 'r) event\<^sub>p\<^sub>t\<^sub>i\<^sub>c\<^sub>k set \<Rightarrow> ('a, 'r) event\<^sub>p\<^sub>t\<^sub>i\<^sub>c\<^sub>k set \<Rightarrow> ('a, 'r) event\<^sub>p\<^sub>t\<^sub>i\<^sub>c\<^sub>k" where
            f6: "\<forall>E Ea. (E \<inter> Ea \<noteq> {} \<or> (\<forall>e. e \<notin> E \<or> e \<notin> Ea)) \<and> (E \<inter> Ea = {} \<or> ee Ea E \<in> E \<and> ee Ea E \<in> Ea)"
            by (metis (no_types) disjoint_iff)
          obtain ees :: "('a, 'r) event\<^sub>p\<^sub>t\<^sub>i\<^sub>c\<^sub>k list \<Rightarrow> ('a, 'r) event\<^sub>p\<^sub>t\<^sub>i\<^sub>c\<^sub>k list \<Rightarrow> ('a, 'r) event\<^sub>p\<^sub>t\<^sub>i\<^sub>c\<^sub>k list" where
            "\<forall>x0 x1. (\<exists>v2. x0 = x1 @ v2) = (x0 = x1 @ ees x0 x1)"
            by moura
          then have f7: "\<forall>es esa. \<not> es \<le> esa \<or> esa = es @ ees esa es"
            by (meson Prefix_Order.prefixE)
          have "{e \<in> set (SOME es. \<exists>esa. ftF esa \<and> (\<forall>e. e \<in> range tick \<longrightarrow> e \<notin> set es) \<and> trace_hide t (ev ` A) @ ua = trace_hide es (ev ` A) @ esa \<and> es \<in> \<D> (Y k)). e \<notin> ev ` A} \<subseteq> set (SOME es. \<exists>esa. ftF esa \<and> (\<forall>e. e \<in> range tick \<longrightarrow> e \<notin> set es) \<and> trace_hide t (ev ` A) @ ua = trace_hide es (ev ` A) @ esa \<and> es \<in> \<D> (Y k))"
            by blast
          then have f8: "range tick \<inter> {e \<in> set (SOME es. \<exists>esa. ftF esa \<and> (\<forall>e. e \<in> range tick \<longrightarrow> e \<notin> set es) \<and> trace_hide t (ev ` A) @ ua = trace_hide es (ev ` A) @ esa \<and> es \<in> \<D> (Y k)). e \<notin> ev ` A} = {}"
            using f6 a1 by (meson subset_iff)
          have "trace_hide (f' m) (ev ` A) @ trace_hide (ees (SOME es. \<exists>esa. ftF esa \<and> (\<forall>e. e \<in> range tick \<longrightarrow> e \<notin> set es) \<and> trace_hide t (ev ` A) @ ua = trace_hide es (ev ` A) @ esa \<and> es \<in> \<D> (Y k)) (f' m)) (ev ` A) = trace_hide (SOME es. \<exists>esa. ftF esa \<and> (\<forall>e. e \<in> range tick \<longrightarrow> e \<notin> set es) \<and> trace_hide t (ev ` A) @ ua = trace_hide es (ev ` A) @ esa \<and> es \<in> \<D> (Y k)) (ev ` A)"
            using f7 a4 by (metis (no_types, lifting) filter_append)
          then have f9: "tF (trace_hide (f' m) (ev ` A) @ trace_hide (ees (SOME es. \<exists>esa. ftF esa \<and> (\<forall>e. e \<in> range tick \<longrightarrow> e \<notin> set es) \<and> trace_hide t (ev ` A) @ ua = trace_hide es (ev ` A) @ esa \<and> es \<in> \<D> (Y k)) (f' m)) (ev ` A))"
            using f8 by (simp add: tickFree_def)
          have "tF (f' m)"
            using f7 f6 a4 a1 by (metis (no_types, lifting) tickFree_append_iff tickFree_def)
          then have f10: "\<exists>es. ftF es \<and> trace_hide t (ev ` A) @ ua = trace_hide (f' m) (ev ` A) @ es \<and> (v1_5 \<notin> range tick \<or> v1_5 \<notin> set (f' m))"
            using f9 f7 f6 a5 a4 a3
            by (smt (z3) append.assoc filter_append front_tickFree_append tickFree_append_iff tickFree_def)
          obtain eea :: "('a, 'r) event\<^sub>p\<^sub>t\<^sub>i\<^sub>c\<^sub>k" where
            "(\<exists>v1. v1 \<in> range tick \<and> v1 \<in> set (f' m)) = (eea \<in> range tick \<and> eea \<in> set (f' m))"
            by moura
          then show ?thesis
            using f10 a2 by (metis \<open>tF (f' m)\<close> disjoint_iff tickFree_def)
        qed *)
      show ?thesis
        apply(rule_tac x="f' m" in exI, rule_tac x=u in exI)
        apply(simp add:oo, rule disjI2, rule_tac x="λn. f' (n + m)" in exI)
        using gg jj kk mm apply (auto simp add: strict_mono_def dual_order.antisym mono_def)
        by (metis plus_nat.add_0 rangeI)
    qed
  qed
  show ?case 
  proof (cases "∃ xa t u f. ftF u ∧ tF t ∧ (∀ i. f i ∉ D (Y xa)) ∧ t ∈ range f ∧
                            x = trace_hide t (ev ` A) @ u ∧ isInfHiddenRun f (Y xa) A")
    case True
    then show ?thesis using aa by blast
  next
    case False
    have dd:"∀xa. ∃t u. ftF u ∧ tF t ∧ x = trace_hide t (ev ` A) @ u ∧
             (t ∈ D (Y xa) ∨ (∃f. isInfHiddenRun f (Y xa) A ∧ (∃i. f i ∈ D (Y xa)) ∧ t ∈ range f))" 
      (is "∀xa. ?dd xa")
    proof (rule_tac allI)
      fix xa
      from 1(3) obtain t u where 
        "ftF u ∧ tF t ∧ x = trace_hide t (ev ` A) @ u ∧
              (t ∈ D (Y xa) ∨ (∃f. isInfHiddenRun f (Y xa) A ∧ t ∈ range f))" 
        by blast
      thus "?dd xa"
        apply(rule_tac x=t in exI, rule_tac x=u in exI, intro conjI, simp_all, elim conjE disjE, simp_all)
        using 1(1) False D_T chain_lemma le_approx2T by blast
    qed
    hence ee:"∀xa. ∃t u. ftF u ∧ tF t ∧ x = trace_hide t (ev ` A) @ u ∧ t ∈ D(Y xa)"
      using bb by blast
    with cc show ?thesis by simp
  qed
qed

lemma Cont_Hiding_prem : ‹(⊔ i. Y i) \ A = (⊔ i. (Y i \ A))› if ‹finite A› ‹chain Y›
proof (subst Process_eq_spec_optimized, safe)
  show ‹s ∈ D ((⊔ i. Y i) \ A) ==> s ∈ D (⊔ i. (Y i \ A))› for s
    by (simp add: limproc_is_thelub chain_Hiding ‹chain Y› D_Hiding D_LUB T_LUB) blast
next
  show ‹s ∈ D (⊔ i. (Y i \ A)) ==> s ∈ D ((⊔ i. Y i) \ A)› for s
    using div_Hiding_lub[OF ‹finite A› ‹chain Y›] by auto
next
  show ‹(s, X) ∈ F ((⊔ i. Y i) \ A) ==> (s, X) ∈ F (⊔ i. (Y i \ A))› for s X
    by (simp add: limproc_is_thelub chain_Hiding ‹chain Y› F_Hiding F_LUB D_LUB T_LUB) blast
next
  assume same_div : ‹D ((⊔ i. Y i) \ A) = D (⊔ i. (Y i \ A))›
  fix s X assume ‹(s, X) ∈ F (⊔ i. (Y i \ A))›
  show ‹(s, X) ∈ F ((⊔ i. Y i) \ A)›
  proof (cases ‹s ∈ D (⊔ i. (Y i \ A))›)
    show ‹s ∈ D (⊔i. Y i \ A) ==> (s, X) ∈ F ((⊔i. Y i) \ A)›
      by (simp add: is_processT8 same_div)
  next
    assume ‹s ∉ D (⊔i. Y i \ A)›
    then obtain j where ‹s ∉ D (Y j \ A)›
      by (auto simp add: limproc_is_thelub chain_Hiding ‹chain Y› D_LUB)
    moreover from ‹(s, X) ∈ F (⊔ i. (Y i \ A))› have ‹(s, X) ∈ F (Y j \ A)›
      by (simp add: limproc_is_thelub chain_Hiding ‹chain Y› F_LUB)
    ultimately show ‹(s, X) ∈ F ((⊔i. Y i) \ A)›
      by (fact le_approx2[OF mono_Hiding[OF is_ub_thelub[OF ‹chain Y›]], THEN iffD2])
  qed
qed



lemma Hiding_cont[simp]:  ‹cont (λa. f a \ A)› if ‹finite A› and ‹cont f›
proof (rule cont_compose[where f = f])
  show ‹cont (λa. a \ A)›
  proof (rule contI2)
    show ‹monofun (λa. a \ A)› by (simp add: mono_Hiding monofunI)
  next
    show ‹chain Y ==> (⊔i. Y i) \ A ⊑ (⊔i. Y i \ A)›
      for Y :: ‹nat ==> ('a, 'r) process_ptick›
      by (simp add: Cont_Hiding_prem[OF ‹finite A›])
  qed
next
  from ‹cont f› show ‹cont f› .
qed



(* TODO : move this *)


lemma length_strict_mono: ‹strict_mono f ==> i + length (f 0) ≤ length (f i)›
  for f :: ‹nat ==> 'a list›
  by (induct i)
    (simp_all add: Suc_le_eq less_length_mono order_le_less_trans strict_mono_Suc_iff)


lemma mono_trace_hide: ‹a ≤ b ==> trace_hide a (ev ` A) ≤ trace_hide b (ev ` A)›
  by (metis prefixE prefixI filter_append)

lemma mono_constant: 
  assumes "mono (f::nat ==> ('a, 'r) event_ptick list)" and "∀i. f i ≤ a"
  shows "∃i. ∀j≥i. f j = f i"
proof -
  from assms(2) have "∀i. length (f i) ≤ length a"
    by (simp add: le_length_mono)
  hence aa:"finite {length (f i)|i. True}"
    using finite_nat_set_iff_bounded_le by auto
  define lm where l2:"lm = Max {length (f i)|i. True}"
  with aa obtain im where "length (f im) = lm" using Max_in by fastforce
  with l2 assms(1) show ?thesis
    apply (intro exI[of _ im], intro impI allI)
    by (metis (mono_tags, lifting) Max_ge aa antisym le_length_mono le_neq_trans less_length_mono
        mem_Collect_eq mono_def order_less_irrefl)
qed

text ‹We can actually optimize the divergences of the const‹Hiding› operator.›

lemma mono_take : ‹s ≤ t ==> take n s ≤ take n t›
  unfolding less_eq_list_def prefix_def by auto

lemma shift_isInfHiddenRun : ‹∃f. isInfHiddenRun f P A ∧ t = f 0›
  if ‹isInfHiddenRun f P A ∧ t ∈ range f›
proof -
  from that obtain i where ‹t = f i› by blast
  hence ‹t = f (i + 0)› by simp
  moreover have ‹isInfHiddenRun (λj. f (i + j)) P A›
    by (metis add_Suc_right strict_mono_Suc_iff that)
  ultimately show ‹∃f. isInfHiddenRun f P A ∧ t = f 0› by blast
qed

lemma uniformize_length_isInfHiddenRun :
  assumes * : ‹isInfHiddenRun f P A› ‹t = f 0›
  defines ‹g ≡ λi. take (i + length t) (f i)›
  shows ‹isInfHiddenRun g P A ∧ (∀i. length (g i) = i + length t) ∧ t = g 0›
proof (intro conjI allI)
  show ‹strict_mono g›
  proof (unfold strict_mono_Suc_iff, rule allI)
    fix i
    from "*"(1) have ‹strict_mono f› by blast
    from length_strict_mono[of f ‹Suc i›, OF ‹strict_mono f›]
    have $ : ‹take (i + length (f 0)) (f (Suc i)) < take ((Suc i) + length (f 0)) (f (Suc i))›
      by (simp add: take_Suc_conv_app_nth)
    from ‹strict_mono f›[THEN strict_monoD, of i ‹Suc i›, simplified]
    obtain u where ‹f (Suc i) = f i @ u› by (meson strict_prefixE')
    with length_strict_mono[of f i, OF ‹strict_mono f›]
    have ‹take (i + length (f 0)) (f i) = take (i + length (f 0)) (f (Suc i))› by simp
    with "$" "*"(2) show ‹g i < g (Suc i)› unfolding g_def by presburger
  qed
next
  show ‹g i ∈ T P› for i unfolding g_def
    by (metis "*"(1) prefixI append_take_drop_id is_processT3_TR)
next
  show ‹trace_hide (g i) (ev ` A) = trace_hide (g 0) (ev ` A)› for i
  proof (rule order_antisym)
    have ‹f 0 ≤ f i› by (simp add: "*"(1) strict_mono_less_eq)
    hence ‹f 0 ≤ take (i + length t) (f i)›
      by (metis "*"(2) prefixE prefixI le_add2 take_all_iff take_append)
    from mono_trace_hide[OF this]
    show ‹trace_hide (g i) (ev ` A) ≤ trace_hide (g 0) (ev ` A)›
      unfolding g_def
      by (metis "*" prefixI append_take_drop_id filter_append le_add2 take_all_iff)
  next
    have $ : ‹take (i + length (f 0)) (f i) ≤ f i› by (metis prefixI append_take_drop_id)
    have ‹take (length t) (f 0) ≤ take (i + length t) (f 0)›
      ‹take (i + length t) (f 0) ≤ take (i + length t) (f i)›
      by (simp add: "*"(2))
        (meson "*"(1) le_add2 le_add_same_cancel2 mono_take strict_mono_less_eq)
    from order_trans[OF this] have ‹g 0 ≤ g i› unfolding g_def by simp
    thus ‹trace_hide (g 0) (ev ` A) ≤ trace_hide (g i) (ev ` A)› by (fact mono_trace_hide)
  qed
next
  show ‹length (g i) = i + length t› for i by (simp add: "*" g_def length_strict_mono)
next
  show ‹t = g 0› by (simp add: "*"(2) g_def)
qed


abbreviation isInfHiddenRun_optimized ::
  ‹[nat ==> ('a, 'r) event_ptick list, ('a, 'r) process_ptick, 'a set, ('a, 'r) trace_ptick] ==> bool›
  where ‹isInfHiddenRun_optimized f P A t ≡
         strict_mono f ∧ (∀i. f i ∈ T P) ∧ (∀i. f i ∉ D P) ∧
         (∀i. trace_hide (f i) (ev ` A) = trace_hide (f 0) (ev ` A)) ∧
         (∀i. length (f i) = i + length t) ∧ t = f 0›

abbreviation div_hide_optimized :: ‹('a, 'r) process_ptick ==> 'a set ==> ('a, 'r) event_ptick list set›
  where ‹div_hide_optimized P A ≡
         {s. ∃t u. ftF u ∧ tF t ∧
                   s = trace_hide t (ev ` A) @ u ∧
                   (t ∈ D P ∨ (∃f. isInfHiddenRun_optimized f P A t))}›


lemma D_Hiding_optimized : ‹D (P \ A) = div_hide_optimized P A›
proof (unfold D_Hiding, intro subset_antisym subsetI)
  show ‹s ∈ div_hide_optimized P A ==> s ∈ div_hide P A› for s by blast
next
  fix s assume ‹s ∈ div_hide P A›
  then obtain t u
    where * : ‹ftF u› ‹tF t› ‹s = trace_hide t (ev ` A) @ u›
      ‹t ∈ D P ∨ (∃f. isInfHiddenRun f P A ∧ t ∈ range f)› by blast
  from "*"(4) show ‹s ∈ div_hide_optimized P A›
  proof (elim disjE exE)
    from "*"(1, 2, 3) show ‹t ∈ D P ==> s ∈ div_hide_optimized P A› by blast
  next
    fix f assume ‹isInfHiddenRun f P A ∧ t ∈ range f›
    with shift_isInfHiddenRun obtain f where ** : ‹isInfHiddenRun f P A ∧ t = f 0› by blast
    show ‹s ∈ div_hide_optimized P A›
    proof (cases ‹∃i. f i ∈ D P›)
      assume ‹∃i. f i ∈ D P›
      then obtain i where ‹f i ∈ D P› ..
      have ‹trace_hide t (ev ` A) = trace_hide (f i) (ev ` A)› by (metis "**")
      moreover from calculation have ‹tF (f i)› by (metis "*"(2) Hiding_tickFree)
      ultimately show ‹s ∈ div_hide_optimized P A›
        using "*"(1, 3) ‹f i ∈ D P› by blast
    next
      assume ‹∄i. f i ∈ D P›
      from "**" uniformize_length_isInfHiddenRun[of f P A t]
      have ‹isInfHiddenRun (λi. take (i + length t) (f i)) P A ∧
            (∀i. length (take (i + length t) (f i)) = i + length t) ∧
            t = take (0 + length t) (f 0)› by blast
      moreover from ‹∄i. f i ∈ D P› have ‹∀i. take (i + length t) (f i) ∉ D P›
        by (metis "**" append_Nil2 append_take_drop_id
            front_tickFree_nonempty_append_imp is_processT2_TR is_processT7)
      ultimately show ‹s ∈ div_hide_optimized P A› using "*"(1, 2, 3) by blast
    qed
  qed
qed


lemma T_Hiding_optimized :
  ‹T (P \ A) = {trace_hide t (ev ` A) |t. (t, ev ` A) ∈ F P} ∪ div_hide_optimized P A›
  by (unfold T_Hiding, fold D_Hiding, unfold D_Hiding_optimized) (fact refl)



text ‹
Actually, term‹f i› can be rewritten as term‹t @ map x [0..<i]›
where term‹x› is the sequence such that term‹f (Suc i) = f i @ [x i]›.›

definition seqRun :: ‹[('a, 'r) trace_ptick, nat ==> ('a, 'r) event_ptick] ==> nat ==> ('a, 'r) trace_ptick›
  where ‹seqRun t x i ≡ t @ map x [0..<i]›

lemma seqRun_is_rec_nat : ‹seqRun t x = rec_nat t (λi t. t @ [x i])›
proof (rule ext)
  show ‹seqRun t x i = rec_nat t (λi t. t @ [x i]) i› for i
    by (induct i) (simp_all add: seqRun_def)
qed


lemma seqRun_0 [simp] : ‹seqRun t x 0 = t›
  and seqRun_Suc [simp] : ‹seqRun t x (Suc i) = seqRun t x i @ [x i]›
  and seqRun_Nil [simp] : ‹seqRun [] x i = map x [0..<i]›
  and seqRun_Cons [simp] : ‹seqRun (a # t) x i = a # seqRun t x i›
  by (simp_all add: seqRun_def)

lemma strict_mono_seqRun [simp] : ‹strict_mono (seqRun t x)›
  by (simp add: strict_mono_Suc_iff)

lemma length_seqRun [simp] : ‹length (seqRun t x i) = i + length t›
  by (simp add: seqRun_def)

lemma t_le_seqRun [simp] : ‹t ≤ seqRun t x i› by (simp add: seqRun_def)

lemma take_t_le_seqRun [simp] : ‹take i t ≤ seqRun t x j›
  by (induct t, simp_all add: seqRun_def less_eq_list_def prefix_def)
    (metis append.assoc append_Cons append_take_drop_id)

lemma nth_seqRun :
  ‹j < i + length t ==>
   seqRun t x i ! j = (if j < length t then t ! j else x (j - length t))›
  by (simp add: seqRun_def nth_append)

lemma take_seqRun [simp] :
  ‹take j (seqRun t x i) = (if j ≤ length t then take j t else seqRun t x (min i (j - length t)))›
  by (simp add: seqRun_def min_def take_map)


lemma seqRun_eq_iff [simp] : ‹seqRun t x i = seqRun t x j ⟷ i = j›
  by (metis add_right_cancel length_seqRun)

lemma seqRun_le_iff [simp] : ‹seqRun t x i ≤ seqRun t x j ⟷ i ≤ j›
  by (simp add: strict_mono_less_eq)

lemma seqRun_less_iff [simp] : ‹seqRun t x i < seqRun t x j ⟷ i < j›
  by (simp add: strict_mono_less)

lemma trace_hide_is_Nil_iff : ‹trace_hide s A = [] ⟷ set s ⊆ A›
  by (simp add: filter_empty_conv subset_code(1))

lemma trace_hide_seqRun_eq_iff :
  ‹trace_hide (seqRun t x i) A = trace_hide t A ⟷ (∀j<i. x j ∈ A)›
  by (simp add: seqRun_def trace_hide_is_Nil_iff subset_iff image_iff)
    (use atLeastLessThan_iff in blast)


abbreviation isInfHidden_seqRun ::
  ‹[nat ==> ('a, 'r) event_ptick, ('a, 'r) process_ptick, 'a set, ('a, 'r) trace_ptick] ==> bool›
  where ‹isInfHidden_seqRun x P A t ≡ ∀i. seqRun t x i ∈ T P ∧ x i ∈ ev ` A›

abbreviation isInfHidden_seqRun_strong ::
  ‹[nat ==> ('a, 'r) event_ptick, ('a, 'r) process_ptick, 'a set, ('a, 'r) trace_ptick] ==> bool›
  where ‹isInfHidden_seqRun_strong x P A t ≡
         ∀i. seqRun t x i ∈ T P ∧ seqRun t x i ∉ D P ∧ x i ∈ ev ` A›



abbreviation div_hide_seqRun :: ‹('a, 'r) process_ptick ==> 'a set ==> ('a, 'r) event_ptick list set›
  where ‹div_hide_seqRun P A ≡
         {s. ∃t u. ftF u ∧ tF t ∧ s = trace_hide t (ev ` A) @ u ∧
                   (t ∈ D P ∨ (∃x. isInfHidden_seqRun x P A t))}›

lemma D_Hiding_seqRun : ‹D (P \ A) = div_hide_seqRun P A›
proof (intro subset_antisym subsetI)
  fix s assume ‹s ∈ D (P \ A)›
  then obtain t u
    where * : ‹ftF u› ‹tF t› ‹s = trace_hide t (ev ` A) @ u›
      ‹t ∈ D P ∨ (∃f. isInfHiddenRun_optimized f P A t)›
    unfolding D_Hiding_optimized by blast
  show ‹s ∈ div_hide_seqRun P A›
  proof (clarify, intro exI conjI)
    show ‹ftF u› ‹tF t›
      ‹s = trace_hide t (ev ` A) @ u› by (fact "*"(1, 2, 3))+
  next
    from "*"(4) show ‹t ∈ D P ∨ (∃x. isInfHidden_seqRun x P A t)›
    proof (elim disjE exE)
      show ‹t ∈ D P ==> t ∈ D P ∨ (∃x. isInfHidden_seqRun x P A t)› ..
    next
      fix f assume $ : ‹isInfHiddenRun_optimized f P A t›
      define x where ‹x i ≡ f (Suc i) ! (i + length t)› for i
      have $$ : ‹seqRun t x i = f i› for i
      proof (induct i)
        show ‹seqRun t x 0 = f 0› by (simp add: "$")
      next
        fix i assume ‹seqRun t x i = f i›
        from "$" have ‹length (f (Suc i)) = Suc i + length t›
          ‹length (f i) = i + length t› ‹f i ≤ f (Suc i)›
          by (blast, blast, simp add: strict_mono_less_eq)
        then obtain y where ‹f (Suc i) = f i @ [y]›
          by (simp add: less_eq_list_def prefix_def)
            (metis append_eq_append_conv length_Suc_conv_rev)
        with ‹length (f i) = i + length t› have ‹f (Suc i) = f i @ [x i]›
          unfolding x_def by (metis nth_append_length)
        thus ‹seqRun t x (Suc i) = f (Suc i)› by (simp add: ‹seqRun t x i = f i›)
      qed
      have ‹isInfHidden_seqRun x P A t›
      proof (intro allI conjI)
        from "$" "$$" show ‹seqRun t x i ∈ T P› for i by presburger+
      next
        from trace_hide_seqRun_eq_iff[of ‹ev ` A› t x, unfolded "$$"] "$"
        show ‹x i ∈ ev ` A› for i by blast
      qed
      thus ‹t ∈ D P ∨ (∃x. isInfHidden_seqRun x P A t)› by blast
    qed
  qed
next
  fix s assume ‹s ∈ div_hide_seqRun P A›
  then obtain t u
    where * : ‹ftF u› ‹tF t› ‹s = trace_hide t (ev ` A) @ u›
      ‹t ∈ D P ∨ (∃x. isInfHidden_seqRun x P A t)› by blast

  show ‹s ∈ D (P \ A)›
  proof (unfold D_Hiding_optimized)
    from "*"(4) show ‹s ∈ div_hide_optimized P A›
    proof (elim disjE exE)
      from "*"(1, 2, 3) show ‹t ∈ D P ==> s ∈ div_hide_optimized P A› by blast
    next
      fix x assume $ : ‹isInfHidden_seqRun x P A t›
      show ‹s ∈ div_hide_optimized P A›
      proof (cases ‹∃i. seqRun t x i ∈ D P›)
        assume ‹∃i. seqRun t x i ∈ D P›
        then obtain i where ‹2020, DaData,CSIRO (ABN 41 687 119 230))
        show ‹s ∈ div_hide_optimized P A›
        proof (clarify, intro exI conjI)
           show ‹ by (fact "*"(1))
        next
          show ‹tF (seqRun t x i)›
             (metis "  n_ seq
 next
 show ‹s = trace_hide (seqRun t x i) (ev ` A) @ u›
 metis "$" *"(3))trace_h)
 next
 from ‹seqRun t x i ∈ Dfunnum \^><openNum
 show ‹
 qed
 next
 assume ‹∄i. seqRun t x i ∈ D P›
 hence ‹isInfHiddenRun_optimized (seqRun t x) P A t›val ex expand_pos = mk_eq {thm num_};
 by (simp add: trace_hide_seqRun_eq_iff "$")
 with "*"(1, 2, 3) show ‹
 qed
 qed
  mult_ mult_ numeral_pl uminus_numeraltatake_bit_numeral_minus_1_eq
 


  T_Hiding_seqRun :
 <>\
 by (unfold T_Hiding, fold D_Hiding_seqRun D_Hiding) (fact refl)

  F_Hiding_seqRun :
 ‹
 {s, X).\existss= trace_hide t t (ev ` A) \\∧∪
 {(s, X). s ∈ div_hide_seqRun P A}›
 by (unfold F_Hiding, fold D_Hiding_seqRun D_Hiding) (fact refl)


  D_Hiding_seqRunI :
 ‹
 t ∈ D P ∨ (∃x. isInfHidden_seqRun x P A t)] ==> s ∈ D (P \ A)›
 unfolding D_Hiding_seqRun by blast

  D_Hiding_seqRunE :
 assumes ‹s ∈ D (P \ A)›
java.lang.NullPointerException: Cannot invoke "String.equals(Object)" because "brackoff" is null
 ‹ rx. isInfHidden_seqRun_strong x P A t)›
 
 from ‹s ∈ D (P \ A)› obtain t u
 where * : ‹ftF u› ‹tF t› ‹s = trace_hide t (ev ` A) @ u›
 ‹t ∈ D P ∨ (∃x. isInfHidden_seqRun x P A t)› unfolding D_Hiding_seqRun by blast
 from "*"(4) show thesis
 proof (elim disjE exE)
 from "*"(1, 2, 3) that show ‹t ∈ D P ==> thesis› by blast
 next
 fix x assume $ : ‹isInfHidden_seqRun x P A t›
 show thesis
 proof (cases ‹∃i. seqRun t x i ∈ D P›)
 assume ‹∃i. seqRun t x i ∈ D P›
 then obtain i where ‹seqRun t x i ∈ D P› ..
 show thesis
 proof (rule that)
 show ‹ftF u› by (fact "*"(1))
 next
 show ‹tF (seqRun t x i)›
 by (metis "$" append_T_imp_tickFree neq_Nil_conv seqRun_Suc)
 next
 show ‹s = trace_hide (seqRun t x i) (ev ` A) @ u›
 by (simp add: "*"(3)) (metis "$" trace_hide_seqRun_eq_iff)
 next
 from ‹seqRun t x i ∈ D P›
 show ‹seqRun t x i ∈ D P ∨
 (∃y. isInfHidden_seqRun_strong y P A (seqRun t x i))› ..
 qed
 next
 from "*"(1, 2, 3) "$" that show ‹∄i. seqRun t x i ∈ D P ==> thesis› by blast
 qed
 qed
 


  T_Hiding_seqRunE :
 assumes ‹s ∈ T (P \ A)›
 obtains t where ‹s = trace_hide t (ev ` A)› ‹(t, ev ` A) ∈ F P›
 | t u where ‹ftF u› ‹tF t› ‹s = trace_hide t (ev ` A) @ u›
 ‹t ∈ D P ∨ (∃x. isInfHidden_seqRun_strong x P A t)›
  (cases ‹s ∈ D (P \ A)›)
 assume ‹s ∉ D (P \ A)›
 with ‹s ∈ T (P \ A)› have ‹s ∈ {trace_hide t (ev ` A) |t. (t, ev ` A) ∈ F P}›
 unfolding D_Hiding T_Hiding by blast
 with that(1) show thesis by blast
  (elim D_Hiding_seqRunE, presburger)


  butlast_seqRun : ‹butlast (seqRun t x i) = (case i of 0 ==> butlast t
 | Suc j ==> seqRun t x j)›
 by (cases i) simp_all


  isInfHidden_seqRun_imp_tickFree : ‹isInfHidden_seqRun x P A t ==> tF t›
 by (metis append_T_imp_tickFree not_Cons_self2 seqRun_0 seqRun_Suc)

  tickFree_seqRun_iff : ‹tF (seqRun t x i) ⟷ tF t ∧ (∀j<i. is_ev (x j))›
 by (induct i; simp) (metis less_Suc_eq)

  front_tickFree_seqRun_iff :
 ‹ftF (seqRun t x i) ⟷ (case i of 0 ==> ftF t | Suc j ==> tF t ∧ (∀k<j. is_ev (x k)))›
 by (cases i) (simp_all add: front_tickFree_iff_tickFree_butlast tickFree_seqRun_iff)


  Hiding_seqRun_projs = F_Hiding_seqRun D_Hiding_seqRun T_Hiding_seqRun

(*<*)
end
  (*>*)